Commit 2023-06-24 09:34 8b49086d

View on Github →

feat: port LinearAlgebra.CliffordAlgebra.Equivs (#5443)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

added def CliffordAlgebraComplex.Q

added theorem CliffordAlgebraComplex.Q_apply

added def CliffordAlgebraComplex.ofComplex

added theorem CliffordAlgebraComplex.ofComplex_I

added theorem CliffordAlgebraComplex.ofComplex_comp_toComplex

added theorem CliffordAlgebraComplex.ofComplex_conj

added theorem CliffordAlgebraComplex.ofComplex_toComplex

added theorem CliffordAlgebraComplex.reverse_apply

added theorem CliffordAlgebraComplex.reverse_eq_id

added def CliffordAlgebraComplex.toComplex

added theorem CliffordAlgebraComplex.toComplex_comp_ofComplex

added theorem CliffordAlgebraComplex.toComplex_involute

added theorem CliffordAlgebraComplex.toComplex_ofComplex

added theorem CliffordAlgebraComplex.toComplex_ι

added theorem CliffordAlgebraDualNumber.equiv_symm_eps

added theorem CliffordAlgebraDualNumber.equiv_ι

added theorem CliffordAlgebraDualNumber.ι_mul_ι

added def CliffordAlgebraQuaternion.Q

added theorem CliffordAlgebraQuaternion.Q_apply

added def CliffordAlgebraQuaternion.ofQuaternion

added theorem CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion

added theorem CliffordAlgebraQuaternion.ofQuaternion_mk

added theorem CliffordAlgebraQuaternion.ofQuaternion_star

added theorem CliffordAlgebraQuaternion.ofQuaternion_toQuaternion

added def CliffordAlgebraQuaternion.quaternionBasis

added def CliffordAlgebraQuaternion.toQuaternion

added theorem CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion

added theorem CliffordAlgebraQuaternion.toQuaternion_ofQuaternion

added theorem CliffordAlgebraQuaternion.toQuaternion_star

added theorem CliffordAlgebraQuaternion.toQuaternion_ι

added theorem CliffordAlgebraRing.involute_eq_id

added theorem CliffordAlgebraRing.reverse_apply

added theorem CliffordAlgebraRing.reverse_eq_id

added theorem CliffordAlgebraRing.ι_eq_zero