Commit 2025-01-24 00:30 08dea193

View on Github →

chore(Mathlib/Algebra/Quaternion): Generalize Quaternion Algebra (#20657)

Estimated changes

Modified Mathlib/Algebra/Quaternion.lean

modified theorem Cardinal.mk_quaternionAlgebra

modified theorem Cardinal.mk_quaternionAlgebra_of_infinite

modified theorem Cardinal.mk_univ_quaternionAlgebra

modified def Quaternion.equivProd

modified def Quaternion.equivTuple

modified theorem Quaternion.equivTuple_apply

modified theorem Quaternion.im_star

modified theorem Quaternion.star_re

modified def Quaternion

modified theorem QuaternionAlgebra.algebraMap_eq

modified theorem QuaternionAlgebra.algebraMap_injective

modified def QuaternionAlgebra.coe

modified theorem QuaternionAlgebra.coe_add

modified theorem QuaternionAlgebra.coe_algebraMap

modified theorem QuaternionAlgebra.coe_basisOneIJK_repr

modified theorem QuaternionAlgebra.coe_im

modified theorem QuaternionAlgebra.coe_imI

modified theorem QuaternionAlgebra.coe_imJ

modified theorem QuaternionAlgebra.coe_imK

modified theorem QuaternionAlgebra.coe_inj

modified theorem QuaternionAlgebra.coe_injective

modified theorem QuaternionAlgebra.coe_intCast

modified theorem QuaternionAlgebra.coe_linearEquivTuple

modified theorem QuaternionAlgebra.coe_linearEquivTuple_symm

modified theorem QuaternionAlgebra.coe_mul

modified theorem QuaternionAlgebra.coe_natCast

modified theorem QuaternionAlgebra.coe_neg

added theorem QuaternionAlgebra.coe_ofNat

modified theorem QuaternionAlgebra.coe_one

modified theorem QuaternionAlgebra.coe_pow

modified theorem QuaternionAlgebra.coe_re

modified theorem QuaternionAlgebra.coe_starAe

modified theorem QuaternionAlgebra.coe_sub

modified theorem QuaternionAlgebra.coe_zero

added theorem QuaternionAlgebra.comm

modified theorem QuaternionAlgebra.eq_re_iff_mem_range_coe

modified theorem QuaternionAlgebra.eq_re_of_eq_coe

modified def QuaternionAlgebra.equivProd

modified def QuaternionAlgebra.equivTuple

modified theorem QuaternionAlgebra.equivTuple_apply

modified theorem QuaternionAlgebra.finrank_eq_four

modified def QuaternionAlgebra.im

modified def QuaternionAlgebra.imIₗ

modified def QuaternionAlgebra.imJₗ

modified def QuaternionAlgebra.imKₗ

modified theorem QuaternionAlgebra.intCast_im

modified theorem QuaternionAlgebra.intCast_imI

modified theorem QuaternionAlgebra.intCast_imJ

modified theorem QuaternionAlgebra.intCast_imK

modified theorem QuaternionAlgebra.intCast_re

modified def QuaternionAlgebra.linearEquivTuple

modified theorem QuaternionAlgebra.mk.eta

modified theorem QuaternionAlgebra.mul_imI

modified theorem QuaternionAlgebra.mul_imJ

modified theorem QuaternionAlgebra.mul_imK

modified theorem QuaternionAlgebra.mul_re

modified theorem QuaternionAlgebra.natCast_im

modified theorem QuaternionAlgebra.natCast_imI

modified theorem QuaternionAlgebra.natCast_imJ

modified theorem QuaternionAlgebra.natCast_imK

modified theorem QuaternionAlgebra.natCast_re

modified theorem QuaternionAlgebra.neg_mk

added theorem QuaternionAlgebra.ofNat_im

added theorem QuaternionAlgebra.ofNat_imI

added theorem QuaternionAlgebra.ofNat_imJ

added theorem QuaternionAlgebra.ofNat_imK

added theorem QuaternionAlgebra.ofNat_re

modified theorem QuaternionAlgebra.one_im

modified theorem QuaternionAlgebra.one_imI

modified theorem QuaternionAlgebra.one_imJ

modified theorem QuaternionAlgebra.one_imK

modified theorem QuaternionAlgebra.one_re

modified theorem QuaternionAlgebra.rank_eq_four

modified theorem QuaternionAlgebra.re_star

modified def QuaternionAlgebra.reₗ

modified theorem QuaternionAlgebra.self_add_star'

modified theorem QuaternionAlgebra.self_add_star

modified theorem QuaternionAlgebra.smul_coe

modified def QuaternionAlgebra.starAe

modified theorem QuaternionAlgebra.star_add_self'

modified theorem QuaternionAlgebra.star_add_self

modified theorem QuaternionAlgebra.star_coe

modified theorem QuaternionAlgebra.star_eq_neg

modified theorem QuaternionAlgebra.star_eq_self

modified theorem QuaternionAlgebra.star_eq_two_re_sub

modified theorem QuaternionAlgebra.star_im

modified theorem QuaternionAlgebra.star_mk

added theorem QuaternionAlgebra.star_smul'

modified theorem QuaternionAlgebra.star_smul

modified def QuaternionAlgebra.swapEquiv

modified theorem QuaternionAlgebra.zero_im

modified theorem QuaternionAlgebra.zero_imI

modified theorem QuaternionAlgebra.zero_imJ

modified theorem QuaternionAlgebra.zero_imK

modified theorem QuaternionAlgebra.zero_re

modified structure QuaternionAlgebra

Modified Mathlib/Algebra/QuaternionBasis.lean

modified def QuaternionAlgebra.Basis.compHom

modified theorem QuaternionAlgebra.Basis.i_mul_k

modified theorem QuaternionAlgebra.Basis.j_mul_k

modified theorem QuaternionAlgebra.Basis.k_mul_j

modified theorem QuaternionAlgebra.Basis.k_mul_k

modified def QuaternionAlgebra.Basis.lift

modified def QuaternionAlgebra.Basis.liftHom

modified theorem QuaternionAlgebra.Basis.lift_add

modified theorem QuaternionAlgebra.Basis.lift_mul

modified theorem QuaternionAlgebra.Basis.lift_one

modified theorem QuaternionAlgebra.Basis.lift_smul

modified theorem QuaternionAlgebra.Basis.lift_zero

modified structure QuaternionAlgebra.Basis

modified theorem QuaternionAlgebra.hom_ext

modified def QuaternionAlgebra.lift

Modified Mathlib/Analysis/Quaternion.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

modified def CliffordAlgebraQuaternion.ofQuaternion

modified theorem CliffordAlgebraQuaternion.ofQuaternion_star

modified def CliffordAlgebraQuaternion.quaternionBasis

modified def CliffordAlgebraQuaternion.toQuaternion

modified theorem CliffordAlgebraQuaternion.toQuaternion_ofQuaternion