Documentation

Mathlib.Analysis.RCLike.Lemmas

Further lemmas about RCLike #

source
theorem convex_RCLike_iff_convex_real {K : Type u_1} {E : Type u_2} [RCLike K] [AddCommMonoid E] [Module K E] [Module ℝ E] [IsScalarTower ℝ K E] {s : Set E} :
Convex K s ↔ Convex ℝ s
source
theorem Polynomial.ofReal_eval {K : Type u_1} [RCLike K] (p : Polynomial ℝ) (x : ℝ) :
↑(eval x p) = (aeval ↑x) p
source
theorem RCLike.span_one_I (K : Type u_1) [RCLike K] :
Submodule.span ℝ {1, I} = ⊤
source
theorem RCLike.rank_le_two (K : Type u_1) [RCLike K] :
Module.rank ℝ K ≤ 2
source
theorem RCLike.finrank_le_two (K : Type u_1) [RCLike K] :
Module.finrank ℝ K ≤ 2
source
def FiniteDimensional.Mathlib.LibraryNote.«RCLike instance» :
LibraryNote

This instance generates a type-class problem with a metavariable ?m that should satisfy RCLike ?m. Since this can only be satisfied by ℝ or ℂ, this does not cause problems.

Equations
Instances For
    source
    instance FiniteDimensional.rclike_to_real {K : Type u_1} [RCLike K] :
    FiniteDimensional ℝ K

    An RCLike field is finite-dimensional over ℝ, since it is spanned by {1, I}.

    source
    theorem FiniteDimensional.proper_rclike (K : Type u_1) (E : Type u_2) [RCLike K] [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] :
    ProperSpace E

    A finite-dimensional vector space over an RCLike is a proper metric space.

    This is not an instance because it would cause a search for FiniteDimensional ?x E before RCLike ?x.

    source
    instance FiniteDimensional.RCLike.properSpace_submodule (K : Type u_1) {E : Type u_2} [RCLike K] [NormedAddCommGroup E] [NormedSpace K E] (S : Submodule K E) [FiniteDimensional K ↥S] :
    ProperSpace ↥S
    source
    @[simp]
    theorem RCLike.reCLM_norm {K : Type u_1} [RCLike K] :
    ‖reCLM‖ = 1
    source
    @[simp]
    theorem RCLike.conjCLE_norm {K : Type u_1} [RCLike K] :
    ‖↑conjCLE‖ = 1
    source
    @[simp]
    theorem RCLike.ofRealCLM_norm {K : Type u_1} [RCLike K] :
    ‖ofRealCLM‖ = 1
    source
    theorem Polynomial.aeval_conj {K : Type u_1} [RCLike K] (p : Polynomial ℝ) (z : K) :
    (aeval ((starRingEnd K) z)) p = (starRingEnd K) ((aeval z) p)
    source
    theorem Polynomial.aeval_ofReal {K : Type u_1} [RCLike K] (p : Polynomial ℝ) (x : ℝ) :
    (aeval ↑x) p = ↑(eval x p)