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.

source
theorem polynomial.of_real_eval {K : Type u_1} [is_R_or_C K] (p : polynomial ℝ) (x : ℝ) :
↑(polynomial.eval x p) = ⇑(polynomial.aeval ↑x) p
source
def library_note.is_R_or_C instance  :
unit

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.

source
@[protected, nolint, instance]
def finite_dimensional.is_R_or_C_to_real {K : Type u_1} [is_R_or_C K] :
finite_dimensional ℝ K

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

source
theorem finite_dimensional.proper_is_R_or_C (K : Type u_1) (E : Type u_2) [is_R_or_C K] [normed_add_comm_group E] [normed_space K E] [finite_dimensional K E] :
proper_space E

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.

source
@[protected, instance]
def finite_dimensional.is_R_or_C.proper_space_submodule (K : Type u_1) {E : Type u_2} [is_R_or_C K] [normed_add_comm_group E] [normed_space K E] (S : submodule K E) [finite_dimensional K ↥S] :
proper_space ↥S
source
@[simp]
theorem is_R_or_C.re_clm_norm {K : Type u_1} [is_R_or_C K] :
‖is_R_or_C.re_clm‖ = 1
source
@[simp]
theorem is_R_or_C.conj_cle_norm {K : Type u_1} [is_R_or_C K] :
‖↑is_R_or_C.conj_cle‖ = 1
source
@[simp]
theorem is_R_or_C.of_real_clm_norm {K : Type u_1} [is_R_or_C K] :
‖is_R_or_C.of_real_clm‖ = 1