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

• (_ : FiniteDimensional ℝ K) = (_ : Module.Finite ℝ K)

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

• (_ : ProperSpace ↥S) = (_ : ProperSpace ↥S)

@[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