mathlib3 documentation

data.is_R_or_C.lemmas

Further lemmas about is_R_or_C #

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 or , this does not cause problems.

@[protected, nolint, instance]

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

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 is_R_or_C ?x.

@[simp]