Grading

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

Statistics

Metric	Count
Definitions liftι, ι, gradedAlgebra	3
Theorems liftι_eq, ι_apply, ι_sq_zero, instGradedMonoidNatSubmoduleExteriorPower, ιMulti_span	5
Total	8

ExteriorAlgebra

Definitions

Name	Category	Theorems
gradedAlgebra 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instGradedMonoidNatSubmoduleExteriorPower 📖	mathematical	—	SetLike.GradedMonoid ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule Submodule.setLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Nat.instAddMonoid exteriorPower	—	Submodule.nat_power_gradedMonoid RingHomSurjective.ids
ιMulti_span 📖	mathematical	—	Submodule.span ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule Set.range DFunLike.coe AlternatingMap AlternatingMap.instFunLike ιMulti Top.top Submodule Submodule.instTop	—	Submodule.eq_top_iff' DirectSum.Decomposition.inductionOn Submodule.addSubmonoidClass Submodule.zero_mem Set.mem_of_mem_of_subset ιMulti_span_fixedDegree Submodule.span_mono Submodule.add_mem

ExteriorAlgebra.GradedAlgebra

Definitions

Name	Category	Theorems
liftι 📖	CompOp	1 math math: liftι_eq
ι 📖	CompOp	2 math math: ι_sq_zero, ι_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftι_eq 📖	mathematical	—	DFunLike.coe AlgHom ExteriorAlgebra DirectSum Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Ring.toSemiring DirectSum.semiring Nat.instAddMonoid SetLike.gsemiring Submodule.addSubmonoidClass ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower instAlgebraCliffordAlgebra DirectSum.instAlgebra Submodule.module Submodule.galgebra AlgHom.funLike liftι AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike DirectSum.of	—	Submodule.addSubmonoidClass ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower Submodule.pow_induction_on_left' Submodule.algebraMap_mem AlgHom.commutes IsScalarTower.right AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SetLike.GradedMonoid.toGradedMul map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass Submodule.mul_mem_mul pow_succ' map_mul NonUnitalAlgSemiHomClass.toMulHomClass ι_sq_zero ExteriorAlgebra.lift_ι_apply DirectSum.of_mul_of DirectSum.of_eq_of_gradedMonoid_eq Sigma.subtype_ext add_comm
ι_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring DirectSum ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module LinearMap.instFunLike ι AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike DirectSum.of ExteriorAlgebra.ι	—	—
ι_sq_zero 📖	mathematical	—	DirectSum ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule CliffordAlgebra.instModule SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid DirectSum.instMul SetLike.gnonUnitalNonAssocSemiring Submodule.addSubmonoidClass SetLike.GradedMonoid.toGradedMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Nat.instAddMonoid ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower DFunLike.coe LinearMap RingHom.id instAddCommMonoidDirectSum DirectSum.instModule Submodule.module LinearMap.instFunLike ι MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass DirectSum.instNonUnitalNonAssocSemiring	—	Submodule.addSubmonoidClass SetLike.GradedMonoid.toGradedMul ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower ι_apply DirectSum.of_mul_of DFinsupp.single_eq_zero ExteriorAlgebra.ι_sq_zero

---

← Back to Index