Further lemmas about RCLike

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

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] : ‖RCLike.reCLM‖ = 1

@[simp]

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

@[simp]

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

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

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