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 Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Submodule.setLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra 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 Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid DirectSum.semiring Nat.instAddMonoid SetLike.gsemiring Submodule.addSubmonoidClass ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower 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 Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra 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 Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid DirectSum.instMul SetLike.gnonUnitalNonAssocSemiring Submodule.addSubmonoidClass SetLike.GradedMonoid.toGradedMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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