Grading

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

Statistics

Metric	Count
Definitions ι, gradedAlgebra	2
Theorems ι_apply	1
Total	3

TensorAlgebra

Definitions

Name	Category	Theorems
gradedAlgebra 📖	CompOp	—

TensorAlgebra.GradedAlgebra

Definitions

Name	Category	Theorems
ι 📖	CompOp	1 math math: ι_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ι_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring DirectSum TensorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.instMembership Submodule.setLike Submodule.instPowNat IsScalarTower.right LinearMap.range RingHomSurjective.ids TensorAlgebra.ι Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module LinearMap.instFunLike ι AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike DirectSum.of	—	IsScalarTower.left IsScalarTower.right RingHomSurjective.ids

---

← Back to Index