theorem
Polynomial.ofReal_eval
{K : Type u_1}
[IsROrC K]
(p : Polynomial ℝ)
(x : ℝ)
:
↑(Polynomial.eval x p) = ↑(Polynomial.aeval ↑x) p
An IsROrC field is finite-dimensional over ℝ, since it is spanned by {1, I}.
theorem
FiniteDimensional.proper_isROrC
(K : Type u_1)
(E : Type u_2)
[IsROrC K]
[NormedAddCommGroup E]
[NormedSpace K E]
[FiniteDimensional K 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 { x // x ∈ S }]
:
ProperSpace { x // x ∈ S }