Further lemmas about IsROrC

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

instance FiniteDimensional.isROrC_to_real {K : Type u_1} [IsROrC K] : FiniteDimensional ℝ K

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

Equations

• ⋯ = ⋯

theorem FiniteDimensional.proper_isROrC (K : Type u_1) (E : Type u_2) [IsROrC K] [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] : ProperSpace E

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

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

instance FiniteDimensional.IsROrC.properSpace_submodule (K : Type u_1) {E : Type u_2} [IsROrC K] [NormedAddCommGroup E] [NormedSpace K E] (S : Submodule K E) [FiniteDimensional K ↥S] : ProperSpace ↥S

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

theorem Polynomial.aeval_conj {K : Type u_1} [IsROrC 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} [IsROrC K] (p : Polynomial ℝ) (x : ℝ) : (Polynomial.aeval ↑x) p = ↑(Polynomial.eval x p)