Further lemmas about RCLike

theorem Polynomial.ofReal_eval {K : Type u_1} [RCLike K] (p : Polynomial ℝ) (x : ℝ) : ↑(eval x p) = (aeval ↑x) p

theorem RCLike.span_one_I (K : Type u_1) [RCLike K] : Submodule.span ℝ {1, I} = ⊤

theorem RCLike.rank_le_two (K : Type u_1) [RCLike K] : Module.rank ℝ K ≤ 2

theorem RCLike.finrank_le_two (K : Type u_1) [RCLike K] : Module.finrank ℝ K ≤ 2

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}.

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.

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

@[simp]

theorem RCLike.reCLM_norm {K : Type u_1} [RCLike K] : ‖reCLM‖ = 1

@[simp]

theorem RCLike.conjCLE_norm {K : Type u_1} [RCLike K] : ‖↑conjCLE‖ = 1

@[simp]

theorem RCLike.ofRealCLM_norm {K : Type u_1} [RCLike K] : ‖ofRealCLM‖ = 1

theorem Polynomial.aeval_conj {K : Type u_1} [RCLike K] (p : Polynomial ℝ) (z : K) : (aeval ((starRingEnd K) z)) p = (starRingEnd K) ((aeval z) p)

theorem Polynomial.aeval_ofReal {K : Type u_1} [RCLike K] (p : Polynomial ℝ) (x : ℝ) : (aeval ↑x) p = ↑(eval x p)