Commit 2023-07-08 09:58 508cf503

View on Github →

feat: port LinearAlgebra.CliffordAlgebra.EvenEquiv (#5600)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

added def CliffordAlgebra.EquivEven.Q'

added theorem CliffordAlgebra.EquivEven.Q'_apply

added def CliffordAlgebra.EquivEven.e0

added theorem CliffordAlgebra.EquivEven.e0_mul_e0

added theorem CliffordAlgebra.EquivEven.e0_mul_v_mul_e0

added theorem CliffordAlgebra.EquivEven.involute_e0

added theorem CliffordAlgebra.EquivEven.involute_v

added theorem CliffordAlgebra.EquivEven.neg_e0_mul_v

added theorem CliffordAlgebra.EquivEven.neg_v_mul_e0

added theorem CliffordAlgebra.EquivEven.reverse_e0

added theorem CliffordAlgebra.EquivEven.reverse_v

added def CliffordAlgebra.EquivEven.v

added theorem CliffordAlgebra.EquivEven.v_sq_scalar

added theorem CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0

added theorem CliffordAlgebra.coe_toEven_reverse_involute

added def CliffordAlgebra.equivEven

added def CliffordAlgebra.evenEquivEvenNeg

added def CliffordAlgebra.evenToNeg

added theorem CliffordAlgebra.evenToNeg_comp_evenToNeg

added theorem CliffordAlgebra.evenToNeg_ι

added def CliffordAlgebra.ofEven

added theorem CliffordAlgebra.ofEven_comp_toEven

added theorem CliffordAlgebra.ofEven_ι

added def CliffordAlgebra.toEven

added theorem CliffordAlgebra.toEven_comp_ofEven

added theorem CliffordAlgebra.toEven_ι