Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-29 05:53 56199b7b

View on Github →

feat(linear_algebra/clifford_algebra/even): Universal property and isomorphisms for the even subalgebra (#14790) The main three results here are:

even.lift : even_hom Q A ≃ (clifford_algebra.even Q →ₐ[R] A)
equiv_even : clifford_algebra Q ≃ₐ[R] clifford_algebra.even (Q' Q)
even_equiv_even_neg : clifford_algebra.even Q ≃ₐ[R] clifford_algebra.even (-Q)

Estimated changes

Created src/linear_algebra/clifford_algebra/even.lean

added theorem clifford_algebra.even.alg_hom_ext

added theorem clifford_algebra.even.lift.aux_algebra_map

added theorem clifford_algebra.even.lift.aux_mul

added theorem clifford_algebra.even.lift.aux_one

added theorem clifford_algebra.even.lift.aux_ι

added def clifford_algebra.even.lift

added theorem clifford_algebra.even.lift_ι

added def clifford_algebra.even.ι

added def clifford_algebra.even

added def clifford_algebra.even_hom.compr₂

added structure clifford_algebra.even_hom

added theorem clifford_algebra.even_to_submodule

Created src/linear_algebra/clifford_algebra/even_equiv.lean

added theorem clifford_algebra.coe_to_even_reverse_involute

added def clifford_algebra.equiv_even.Q'

added theorem clifford_algebra.equiv_even.Q'_apply

added def clifford_algebra.equiv_even.e0

added theorem clifford_algebra.equiv_even.e0_mul_e0

added theorem clifford_algebra.equiv_even.e0_mul_v_mul_e0

added theorem clifford_algebra.equiv_even.involute_e0

added theorem clifford_algebra.equiv_even.involute_v

added theorem clifford_algebra.equiv_even.neg_e0_mul_v

added theorem clifford_algebra.equiv_even.neg_v_mul_e0

added theorem clifford_algebra.equiv_even.reverse_e0

added theorem clifford_algebra.equiv_even.reverse_v

added def clifford_algebra.equiv_even.v

added theorem clifford_algebra.equiv_even.v_sq_scalar

added theorem clifford_algebra.equiv_even.ι_eq_v_add_smul_e0

added def clifford_algebra.equiv_even

added def clifford_algebra.even_equiv_even_neg

added def clifford_algebra.even_to_neg

added theorem clifford_algebra.even_to_neg_comp_even_to_neg

added theorem clifford_algebra.even_to_neg_ι

added def clifford_algebra.of_even

added theorem clifford_algebra.of_even_comp_to_even

added theorem clifford_algebra.of_even_ι

added def clifford_algebra.to_even

added theorem clifford_algebra.to_even_comp_of_even

added theorem clifford_algebra.to_even_ι