Further lemmas about
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This instance generates a type-class problem with a metavariable
?m that should satisfy
is_R_or_C ?m. Since this can only be satisfied by
ℂ, this does not cause problems.
@[protected, nolint, instance]
is_R_or_C field is finite-dimensional over
ℝ, since it is spanned by
A finite dimensional vector space over an
is_R_or_C is a proper metric space.
This is not an instance because it would cause a search for
finite_dimensional ?x E before