# Further lemmas about RCLike#

theorem Polynomial.ofReal_eval {K : Type u_1} [] (p : ) (x : ) :
() = () p
instance FiniteDimensional.rclike_to_real {K : Type u_1} [] :

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

Equations
• =
theorem FiniteDimensional.proper_rclike (K : Type u_1) (E : Type u_2) [] [] [] :

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} [] [] (S : ) [] :
Equations
• =
@[simp]
theorem RCLike.reCLM_norm {K : Type u_1} [] :
RCLike.reCLM = 1
@[simp]
theorem RCLike.conjCLE_norm {K : Type u_1} [] :
RCLike.conjCLE = 1
@[simp]
theorem RCLike.ofRealCLM_norm {K : Type u_1} [] :
RCLike.ofRealCLM = 1
theorem Polynomial.aeval_conj {K : Type u_1} [] (p : ) (z : K) :
(Polynomial.aeval (() z)) p = () (() p)
theorem Polynomial.aeval_ofReal {K : Type u_1} [] (p : ) (x : ) :
() p = ()