Commit 2023-06-22 09:57 b90d47b1

View on Github →

feat: port LinearAlgebra.ExteriorAlgebra.Basic (#5375)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

added def ExteriorAlgebra.algebraMapInv

added theorem ExteriorAlgebra.algebraMap_eq_one_iff

added theorem ExteriorAlgebra.algebraMap_eq_zero_iff

added theorem ExteriorAlgebra.algebraMap_inj

added theorem ExteriorAlgebra.algebraMap_leftInverse

added theorem ExteriorAlgebra.comp_ι_sq_zero

added theorem ExteriorAlgebra.hom_ext

added theorem ExteriorAlgebra.induction

added def ExteriorAlgebra.invertibleAlgebraMapEquiv

added theorem ExteriorAlgebra.isUnit_algebraMap

added def ExteriorAlgebra.lift

added theorem ExteriorAlgebra.lift_comp_ι

added theorem ExteriorAlgebra.lift_unique

added theorem ExteriorAlgebra.lift_ι_apply

added def ExteriorAlgebra.toTrivSqZeroExt

added theorem ExteriorAlgebra.toTrivSqZeroExt_ι

added def ExteriorAlgebra.ι

added def ExteriorAlgebra.ιInv

added def ExteriorAlgebra.ιMulti

added theorem ExteriorAlgebra.ιMulti_apply

added theorem ExteriorAlgebra.ιMulti_succ_apply

added theorem ExteriorAlgebra.ιMulti_succ_curryLeft

added theorem ExteriorAlgebra.ιMulti_zero_apply

added theorem ExteriorAlgebra.ι_add_mul_swap

added theorem ExteriorAlgebra.ι_comp_lift

added theorem ExteriorAlgebra.ι_eq_algebraMap_iff

added theorem ExteriorAlgebra.ι_eq_zero_iff

added theorem ExteriorAlgebra.ι_inj

added theorem ExteriorAlgebra.ι_leftInverse

added theorem ExteriorAlgebra.ι_mul_prod_list

added theorem ExteriorAlgebra.ι_ne_one

added theorem ExteriorAlgebra.ι_range_disjoint_one

added theorem ExteriorAlgebra.ι_sq_zero

added def ExteriorAlgebra

added def TensorAlgebra.toExterior

added theorem TensorAlgebra.toExterior_ι