Mathlib Changelog
Changelog
About
Github
Commit
2020-10-14 14:46
442ef226
View on Github →
feat(linear_algebra/clifford_algebra): Add a definition derived from exterior_algebra.lean (
#4430
)
Estimated changes
Created
src/linear_algebra/clifford_algebra.lean
added
def
clifford_algebra.as_exterior
added
theorem
clifford_algebra.comp_ι_square_scalar
added
theorem
clifford_algebra.hom_ext
added
def
clifford_algebra.lift
added
theorem
clifford_algebra.lift_comp_ι
added
theorem
clifford_algebra.lift_unique
added
theorem
clifford_algebra.lift_ι_apply
added
inductive
clifford_algebra.rel
added
def
clifford_algebra.ι
added
theorem
clifford_algebra.ι_comp_lift
added
theorem
clifford_algebra.ι_square_scalar
added
def
clifford_algebra
Modified
src/linear_algebra/exterior_algebra.lean