Commit 2023-05-31 07:01 e9bc9204

View on Github →

feat: port Analysis.Quaternion (#4515)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Quaternion.lean

Created Mathlib/Analysis/Quaternion.lean

added def Quaternion.coeComplex

added theorem Quaternion.coeComplex_add

added theorem Quaternion.coeComplex_coe

added theorem Quaternion.coeComplex_imI

added theorem Quaternion.coeComplex_imJ

added theorem Quaternion.coeComplex_imK

added theorem Quaternion.coeComplex_mul

added theorem Quaternion.coeComplex_one

added theorem Quaternion.coeComplex_re

added theorem Quaternion.coeComplex_zero

added theorem Quaternion.coe_ofComplex

added theorem Quaternion.coe_real_complex_mul

added theorem Quaternion.continuous_coe

added theorem Quaternion.continuous_im

added theorem Quaternion.continuous_imI

added theorem Quaternion.continuous_imJ

added theorem Quaternion.continuous_imK

added theorem Quaternion.continuous_normSq

added theorem Quaternion.continuous_re

added theorem Quaternion.hasSum_coe

added theorem Quaternion.inner_def

added theorem Quaternion.inner_self

added theorem Quaternion.nnnorm_coe

added theorem Quaternion.nnnorm_star

added theorem Quaternion.normSq_eq_norm_mul_self

added theorem Quaternion.norm_coe

added theorem Quaternion.norm_piLp_equiv_symm_equivTuple

added theorem Quaternion.norm_star

added def Quaternion.ofComplex

added theorem Quaternion.summable_coe

added theorem Quaternion.tsum_coe

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Modified Mathlib/Data/Matrix/Rank.lean