Documentation Verification Report

OfAlternating

📁 Source: Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean

Statistics

Metric	Count
Definitions `instModuleAddCommGroup`, `liftAlternating`, `liftAlternatingEquiv`	3
Theorems `lhom_ext`, `lhom_ext_iff`, `liftAlternatingEquiv_apply`, `liftAlternatingEquiv_symm_apply`, `liftAlternating_algebraMap`, `liftAlternating_apply_ιMulti`, `liftAlternating_comp`, `liftAlternating_comp_ιMulti`, `liftAlternating_one`, `liftAlternating_ι`, `liftAlternating_ιMulti`, `liftAlternating_ι_mul`	12
Total	15

AlternatingMap

Definitions

Name	Category	Theorems
`instModuleAddCommGroup` 📖	CompOp	16 math math: `ExteriorAlgebra.liftAlternating_ι_mul`, `exteriorPower.alternatingMapLinearEquiv_ιMulti`, `ExteriorAlgebra.liftAlternating_comp`, `exteriorPower.alternatingMapLinearEquiv_symm_map`, `ExteriorAlgebra.liftAlternatingEquiv_symm_apply`, `ExteriorAlgebra.liftAlternating_ιMulti`, `ExteriorAlgebra.liftAlternatingEquiv_apply`, `ExteriorAlgebra.liftAlternating_apply_ιMulti`, `ExteriorAlgebra.liftAlternating_one`, `exteriorPower.alternatingMapLinearEquiv_apply_ιMulti`, `exteriorPower.alternatingMapLinearEquiv_comp_ιMulti`, `exteriorPower.alternatingMapLinearEquiv_comp`, `ExteriorAlgebra.liftAlternating_comp_ιMulti`, `ExteriorAlgebra.liftAlternating_algebraMap`, `exteriorPower.alternatingMapLinearEquiv_symm_apply`, `ExteriorAlgebra.liftAlternating_ι`

ExteriorAlgebra

Definitions

Name	Category	Theorems
`liftAlternating` 📖	CompOp	9 math math: `liftAlternating_ι_mul`, `liftAlternating_comp`, `liftAlternating_ιMulti`, `liftAlternatingEquiv_apply`, `liftAlternating_apply_ιMulti`, `liftAlternating_one`, `liftAlternating_comp_ιMulti`, `liftAlternating_algebraMap`, `liftAlternating_ι`
`liftAlternatingEquiv` 📖	CompOp	2 math math: `liftAlternatingEquiv_symm_apply`, `liftAlternatingEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lhom_ext` 📖	—	`LinearMap.compAlternatingMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `ιMulti`	—	—	`LinearEquiv.injective` `smulCommClass_self` `RingHomInvPair.ids`
`lhom_ext_iff` 📖	mathematical	—	`LinearMap.compAlternatingMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `ιMulti`	—	`lhom_ext`
`liftAlternatingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `liftAlternatingEquiv` `LinearMap.instFunLike` `liftAlternating`	—	`RingHomInvPair.ids` `smulCommClass_self`
`liftAlternatingEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `LinearMap.addCommMonoid` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `liftAlternatingEquiv` `LinearMap.compAlternatingMap` `ιMulti`	—	`RingHomInvPair.ids` `smulCommClass_self`
`liftAlternating_algebraMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `LinearMap.instFunLike` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `liftAlternating` `RingHom` `RingHom.instFunLike` `algebraMap` `instAlgebraCliffordAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlternatingMap.instFunLike` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smulCommClass_self` `Algebra.algebraMap_eq_smul_one` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `liftAlternating_one`
`liftAlternating_apply_ιMulti` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `LinearMap.instFunLike` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `liftAlternating` `AlternatingMap.instFunLike` `ιMulti`	—	`smulCommClass_self` `ιMulti_apply` `liftAlternating_one` `Unique.instSubsingleton` `Fin.isEmpty'` `liftAlternating_ι_mul` `AlternatingMap.curryLeft_apply_apply` `Matrix.cons_head_tail`
`liftAlternating_comp` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `LinearMap.instFunLike` `liftAlternating` `LinearMap.compAlternatingMap` `LinearMap.comp` `RingHomCompTriple.ids`	—	`LinearMap.ext` `smulCommClass_self` `RingHomCompTriple.ids` `LinearMap.comp_apply` `CliffordAlgebra.left_induction` `liftAlternating_algebraMap` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.compAlternatingMap_apply` `map_add` `SemilinearMapClass.toAddHomClass` `liftAlternating_ι_mul`
`liftAlternating_comp_ιMulti` 📖	mathematical	—	`LinearMap.compAlternatingMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `DFunLike.coe` `LinearMap` `RingHom.id` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `LinearMap.instFunLike` `liftAlternating` `ιMulti`	—	`AlternatingMap.ext` `smulCommClass_self` `liftAlternating_apply_ιMulti`
`liftAlternating_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `LinearMap.instFunLike` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `liftAlternating` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AlternatingMap.instFunLike` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smulCommClass_self` `CliffordAlgebra.foldl_one`
`liftAlternating_ι` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `LinearMap.instFunLike` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `liftAlternating` `ι` `AlternatingMap.instFunLike` `Matrix.vecCons` `Matrix.vecEmpty`	—	`smulCommClass_self` `CliffordAlgebra.foldl_ι` `LinearMap.mk₂_apply` `AlternatingMap.curryLeft_apply_apply` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForallOfFastIsEmpty` `Lean.Meta.instFastIsEmptyFinOfNatNat`
`liftAlternating_ιMulti` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Ring.toAddCommGroup` `CliffordAlgebra.instModule` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `LinearMap.instFunLike` `liftAlternating` `ιMulti` `LinearMap.id`	—	`LinearMap.ext` `smulCommClass_self` `CliffordAlgebra.left_induction` `liftAlternating_algebraMap` `ιMulti_zero_apply` `Algebra.algebraMap_eq_smul_one` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `liftAlternating_ι_mul` `Algebra.to_smulCommClass` `ιMulti_succ_curryLeft` `RingHomCompTriple.ids` `liftAlternating_comp`
`liftAlternating_ι_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ExteriorAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingCliffordAlgebra` `QuadraticForm` `AddCommGroup.toAddCommMonoid` `QuadraticMap.instZero` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `CliffordAlgebra.instModule` `LinearMap.instFunLike` `Pi.addCommMonoid` `AlternatingMap` `AlternatingMap.instAddCommMonoid` `LinearMap.addCommMonoid` `Pi.module` `AlternatingMap.instModuleAddCommGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `liftAlternating` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `ι` `AlternatingMap.instModule` `CommSemiring.toCommMonoid` `AlternatingMap.curryLeft`	—	`smulCommClass_self` `CliffordAlgebra.foldl_mul` `CliffordAlgebra.foldl_ι`

---

← Back to Index