Commit 2023-06-26 01:21 01e12e77

View on Github →

feat: port LinearAlgebra.ExteriorAlgebra.OfAlternating (#5465)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean

added theorem ExteriorAlgebra.lhom_ext

added def ExteriorAlgebra.liftAlternating

added def ExteriorAlgebra.liftAlternatingEquiv

added theorem ExteriorAlgebra.liftAlternating_algebraMap

added theorem ExteriorAlgebra.liftAlternating_apply_ιMulti

added theorem ExteriorAlgebra.liftAlternating_comp

added theorem ExteriorAlgebra.liftAlternating_comp_ιMulti

added theorem ExteriorAlgebra.liftAlternating_one

added theorem ExteriorAlgebra.liftAlternating_ι

added theorem ExteriorAlgebra.liftAlternating_ιMulti

added theorem ExteriorAlgebra.liftAlternating_ι_mul