Commit 2023-05-22 00:38 8c6ccafa

View on Github →

feat: port Algebra.Quaternion (#3776)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Quaternion.lean

added theorem Cardinal.mk_quaternion

added theorem Cardinal.mk_quaternionAlgebra

added theorem Cardinal.mk_quaternionAlgebra_of_infinite

added theorem Cardinal.mk_quaternion_of_infinite

added theorem Cardinal.mk_univ_quaternion

added theorem Cardinal.mk_univ_quaternionAlgebra

added theorem Cardinal.mk_univ_quaternionAlgebra_of_infinite

added theorem Cardinal.mk_univ_quaternion_of_infinite

added theorem Quaternion.add_imI

added theorem Quaternion.add_imJ

added theorem Quaternion.add_imK

added theorem Quaternion.add_re

added theorem Quaternion.algebraMap_def

added def Quaternion.coe

added theorem Quaternion.coe_add

added theorem Quaternion.coe_commute

added theorem Quaternion.coe_commutes

added theorem Quaternion.coe_div

added theorem Quaternion.coe_im

added theorem Quaternion.coe_imI

added theorem Quaternion.coe_imJ

added theorem Quaternion.coe_imK

added theorem Quaternion.coe_inj

added theorem Quaternion.coe_injective

added theorem Quaternion.coe_int_cast

added theorem Quaternion.coe_inv

added theorem Quaternion.coe_mul

added theorem Quaternion.coe_mul_eq_smul

added theorem Quaternion.coe_nat_cast

added theorem Quaternion.coe_neg

added theorem Quaternion.coe_normSq_add

added theorem Quaternion.coe_one

added theorem Quaternion.coe_pow

added theorem Quaternion.coe_rat_cast

added theorem Quaternion.coe_re

added theorem Quaternion.coe_smul

added theorem Quaternion.coe_starAe

added theorem Quaternion.coe_sub

added theorem Quaternion.coe_zero

added theorem Quaternion.coe_zpow

added theorem Quaternion.eq_re_iff_mem_range_coe

added theorem Quaternion.eq_re_of_eq_coe

added def Quaternion.equivProd

added def Quaternion.equivTuple

added theorem Quaternion.equivTuple_apply

added theorem Quaternion.ext

added theorem Quaternion.ext_iff

added theorem Quaternion.finrank_eq_four

added theorem Quaternion.im_idem

added theorem Quaternion.im_imI

added theorem Quaternion.im_imJ

added theorem Quaternion.im_imK

added theorem Quaternion.im_re

added theorem Quaternion.im_sq

added theorem Quaternion.im_star

added theorem Quaternion.int_cast_im

added theorem Quaternion.int_cast_imI

added theorem Quaternion.int_cast_imJ

added theorem Quaternion.int_cast_imK

added theorem Quaternion.int_cast_re

added theorem Quaternion.mul_coe_eq_smul

added theorem Quaternion.mul_imI

added theorem Quaternion.mul_imJ

added theorem Quaternion.mul_imK

added theorem Quaternion.mul_re

added theorem Quaternion.nat_cast_im

added theorem Quaternion.nat_cast_imI

added theorem Quaternion.nat_cast_imJ

added theorem Quaternion.nat_cast_imK

added theorem Quaternion.nat_cast_re

added theorem Quaternion.neg_imI

added theorem Quaternion.neg_imJ

added theorem Quaternion.neg_imK

added theorem Quaternion.neg_re

added def Quaternion.normSq

added theorem Quaternion.normSq_add

added theorem Quaternion.normSq_coe

added theorem Quaternion.normSq_def'

added theorem Quaternion.normSq_def

added theorem Quaternion.normSq_div

added theorem Quaternion.normSq_eq_zero

added theorem Quaternion.normSq_int_cast

added theorem Quaternion.normSq_inv

added theorem Quaternion.normSq_le_zero

added theorem Quaternion.normSq_nat_cast

added theorem Quaternion.normSq_ne_zero

added theorem Quaternion.normSq_neg

added theorem Quaternion.normSq_nonneg

added theorem Quaternion.normSq_rat_cast

added theorem Quaternion.normSq_smul

added theorem Quaternion.normSq_star

added theorem Quaternion.normSq_zpow

added theorem Quaternion.one_im

added theorem Quaternion.one_imI

added theorem Quaternion.one_imJ

added theorem Quaternion.one_imK

added theorem Quaternion.one_re

added theorem Quaternion.rank_eq_four

added theorem Quaternion.rat_cast_im

added theorem Quaternion.rat_cast_imI

added theorem Quaternion.rat_cast_imJ

added theorem Quaternion.rat_cast_imK

added theorem Quaternion.rat_cast_re

added theorem Quaternion.self_mul_star

added theorem Quaternion.smul_coe

added theorem Quaternion.smul_imI

added theorem Quaternion.smul_imJ

added theorem Quaternion.smul_imK

added theorem Quaternion.smul_re

added theorem Quaternion.sq_eq_neg_normSq

added theorem Quaternion.sq_eq_normSq

added def Quaternion.starAe

added theorem Quaternion.star_coe

added theorem Quaternion.star_eq_neg

added theorem Quaternion.star_eq_self

added theorem Quaternion.star_im

added theorem Quaternion.star_imI

added theorem Quaternion.star_imJ

added theorem Quaternion.star_imK

added theorem Quaternion.star_mul_self

added theorem Quaternion.star_re

added theorem Quaternion.star_smul

added theorem Quaternion.sub_imI

added theorem Quaternion.sub_imJ

added theorem Quaternion.sub_imK

added theorem Quaternion.sub_re

added theorem Quaternion.zero_im

added theorem Quaternion.zero_imI

added theorem Quaternion.zero_imJ

added theorem Quaternion.zero_imK

added theorem Quaternion.zero_re

added def Quaternion

added theorem QuaternionAlgebra.add_im

added theorem QuaternionAlgebra.add_imI

added theorem QuaternionAlgebra.add_imJ

added theorem QuaternionAlgebra.add_imK

added theorem QuaternionAlgebra.add_re

added theorem QuaternionAlgebra.algebraMap_eq

added def QuaternionAlgebra.coe

added theorem QuaternionAlgebra.coe_add

added theorem QuaternionAlgebra.coe_algebraMap

added theorem QuaternionAlgebra.coe_basisOneIJK_repr

added theorem QuaternionAlgebra.coe_commute

added theorem QuaternionAlgebra.coe_commutes

added theorem QuaternionAlgebra.coe_im

added theorem QuaternionAlgebra.coe_imI

added theorem QuaternionAlgebra.coe_imJ

added theorem QuaternionAlgebra.coe_imK

added theorem QuaternionAlgebra.coe_inj

added theorem QuaternionAlgebra.coe_injective

added theorem QuaternionAlgebra.coe_int_cast

added theorem QuaternionAlgebra.coe_linearEquivTuple

added theorem QuaternionAlgebra.coe_linearEquivTuple_symm

added theorem QuaternionAlgebra.coe_mul

added theorem QuaternionAlgebra.coe_mul_eq_smul

added theorem QuaternionAlgebra.coe_nat_cast

added theorem QuaternionAlgebra.coe_neg

added theorem QuaternionAlgebra.coe_one

added theorem QuaternionAlgebra.coe_pow

added theorem QuaternionAlgebra.coe_re

added theorem QuaternionAlgebra.coe_smul

added theorem QuaternionAlgebra.coe_starAe

added theorem QuaternionAlgebra.coe_sub

added theorem QuaternionAlgebra.coe_zero

added theorem QuaternionAlgebra.eq_re_iff_mem_range_coe

added theorem QuaternionAlgebra.eq_re_of_eq_coe

added def QuaternionAlgebra.equivProd

added def QuaternionAlgebra.equivTuple

added theorem QuaternionAlgebra.equivTuple_apply

added theorem QuaternionAlgebra.finrank_eq_four

added def QuaternionAlgebra.im

added theorem QuaternionAlgebra.imI_star

added def QuaternionAlgebra.imIₗ

added theorem QuaternionAlgebra.imJ_star

added def QuaternionAlgebra.imJₗ

added theorem QuaternionAlgebra.imK_star

added def QuaternionAlgebra.imKₗ

added theorem QuaternionAlgebra.im_idem

added theorem QuaternionAlgebra.im_imI

added theorem QuaternionAlgebra.im_imJ

added theorem QuaternionAlgebra.im_imK

added theorem QuaternionAlgebra.im_re

added theorem QuaternionAlgebra.im_star

added theorem QuaternionAlgebra.int_cast_im

added theorem QuaternionAlgebra.int_cast_imI

added theorem QuaternionAlgebra.int_cast_imJ

added theorem QuaternionAlgebra.int_cast_imK

added theorem QuaternionAlgebra.int_cast_re

added def QuaternionAlgebra.linearEquivTuple

added theorem QuaternionAlgebra.mk.eta

added theorem QuaternionAlgebra.mk_add_mk

added theorem QuaternionAlgebra.mk_mul_mk

added theorem QuaternionAlgebra.mk_sub_mk

added theorem QuaternionAlgebra.mul_coe_eq_smul

added theorem QuaternionAlgebra.mul_imI

added theorem QuaternionAlgebra.mul_imJ

added theorem QuaternionAlgebra.mul_imK

added theorem QuaternionAlgebra.mul_re

added theorem QuaternionAlgebra.mul_star_eq_coe

added theorem QuaternionAlgebra.nat_cast_im

added theorem QuaternionAlgebra.nat_cast_imI

added theorem QuaternionAlgebra.nat_cast_imJ

added theorem QuaternionAlgebra.nat_cast_imK

added theorem QuaternionAlgebra.nat_cast_re

added theorem QuaternionAlgebra.neg_im

added theorem QuaternionAlgebra.neg_imI

added theorem QuaternionAlgebra.neg_imJ

added theorem QuaternionAlgebra.neg_imK

added theorem QuaternionAlgebra.neg_mk

added theorem QuaternionAlgebra.neg_re

added theorem QuaternionAlgebra.one_im

added theorem QuaternionAlgebra.one_imI

added theorem QuaternionAlgebra.one_imJ

added theorem QuaternionAlgebra.one_imK

added theorem QuaternionAlgebra.one_re

added theorem QuaternionAlgebra.rank_eq_four

added theorem QuaternionAlgebra.re_add_im

added theorem QuaternionAlgebra.re_star

added def QuaternionAlgebra.reₗ

added theorem QuaternionAlgebra.self_add_star'

added theorem QuaternionAlgebra.self_add_star

added theorem QuaternionAlgebra.smul_coe

added theorem QuaternionAlgebra.smul_im

added theorem QuaternionAlgebra.smul_imI

added theorem QuaternionAlgebra.smul_imJ

added theorem QuaternionAlgebra.smul_imK

added theorem QuaternionAlgebra.smul_mk

added theorem QuaternionAlgebra.smul_re

added def QuaternionAlgebra.starAe

added theorem QuaternionAlgebra.star_add_self'

added theorem QuaternionAlgebra.star_add_self

added theorem QuaternionAlgebra.star_coe

added theorem QuaternionAlgebra.star_eq_neg

added theorem QuaternionAlgebra.star_eq_self

added theorem QuaternionAlgebra.star_eq_two_re_sub

added theorem QuaternionAlgebra.star_im

added theorem QuaternionAlgebra.star_mk

added theorem QuaternionAlgebra.star_mul_eq_coe

added theorem QuaternionAlgebra.star_smul

added theorem QuaternionAlgebra.sub_im

added theorem QuaternionAlgebra.sub_imI

added theorem QuaternionAlgebra.sub_imJ

added theorem QuaternionAlgebra.sub_imK

added theorem QuaternionAlgebra.sub_re

added theorem QuaternionAlgebra.sub_self_im

added theorem QuaternionAlgebra.sub_self_re

added theorem QuaternionAlgebra.zero_im

added theorem QuaternionAlgebra.zero_imI

added theorem QuaternionAlgebra.zero_imJ

added theorem QuaternionAlgebra.zero_imK

added theorem QuaternionAlgebra.zero_re

added structure QuaternionAlgebra

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.toNat_ofNat