Documentation Verification Report

Submodule

📁 Source: Mathlib/RingTheory/GradedAlgebra/Homogeneous/Submodule.lean

Statistics

Metric	Count
Definitions `HomogeneousSubmodule`, `setLike`, `toSubmodule`, `IsHomogeneous`, `instPartialOrderHomogeneousSubmodule`, `instPartialOrderHomogeneousSubmodule_1`, `instSetLikeHomogeneousSubmodule`	7
Theorems `ext`, `ext'`, `ext_iff`, `isHomogeneous`, `is_homogeneous'`, `mem_toSubmodule_iff`, `toSubmodule_injective`, `mem_iff`, `instAddSubmonoidClassHomogeneousSubmodule`, `instSMulMemClassHomogeneousSubmodule`	10
Total	17

HomogeneousSubmodule

Definitions

Name	Category	Theorems
`setLike` 📖	CompOp	1 math math: `mem_toSubmodule_iff`
`toSubmodule` 📖	CompOp	9 math math: `is_homogeneous'`, `HomogeneousIdeal.toAddSubmonoid_irrelevant_le`, `mem_toSubmodule_iff`, `HomogeneousIdeal.irrelevant_le`, `isHomogeneous`, `ext_iff`, `HomogeneousIdeal.irrelevant_eq_iSup`, `HomogeneousIdeal.irrelevant_eq_closure`, `toSubmodule_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`toSubmodule`	—	—	`toSubmodule_injective`
`ext'` 📖	—	`HomogeneousSubmodule` `SetLike.instMembership` `setLike`	—	—	`ext` `Submodule.ext` `Submodule.IsHomogeneous.mem_iff` `isHomogeneous`
`ext_iff` 📖	mathematical	—	`toSubmodule`	—	`ext`
`isHomogeneous` 📖	mathematical	—	`Submodule.IsHomogeneous` `toSubmodule`	—	`is_homogeneous'`
`is_homogeneous'` 📖	mathematical	—	`Submodule.IsHomogeneous` `toSubmodule`	—	—
`mem_toSubmodule_iff` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `Submodule.setLike` `toSubmodule` `HomogeneousSubmodule` `setLike`	—	—
`toSubmodule_injective` 📖	mathematical	—	`HomogeneousSubmodule` `Submodule` `toSubmodule`	—	—

Submodule

Definitions

Name	Category	Theorems
`IsHomogeneous` 📖	MathDef	2 math math: `HomogeneousSubmodule.is_homogeneous'`, `HomogeneousSubmodule.isHomogeneous`

Submodule.IsHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_iff` 📖	mathematical	`Submodule.IsHomogeneous`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose`	—	`DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff` `Submodule.addSubmonoidClass`

(root)

Definitions

Name	Category	Theorems
`HomogeneousSubmodule` 📖	CompData	4 math math: `HomogeneousSubmodule.mem_toSubmodule_iff`, `instAddSubmonoidClassHomogeneousSubmodule`, `HomogeneousSubmodule.toSubmodule_injective`, `instSMulMemClassHomogeneousSubmodule`
`instPartialOrderHomogeneousSubmodule` 📖	CompOp	—
`instPartialOrderHomogeneousSubmodule_1` 📖	CompOp	—
`instSetLikeHomogeneousSubmodule` 📖	CompOp	2 math math: `instAddSubmonoidClassHomogeneousSubmodule`, `instSMulMemClassHomogeneousSubmodule`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAddSubmonoidClassHomogeneousSubmodule` 📖	mathematical	—	`AddSubmonoidClass` `HomogeneousSubmodule` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSetLikeHomogeneousSubmodule`	—	`Submodule.add_mem` `Submodule.zero_mem`
`instSMulMemClassHomogeneousSubmodule` 📖	mathematical	—	`SMulMemClass` `HomogeneousSubmodule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instSetLikeHomogeneousSubmodule`	—	`Submodule.smul_mem`

---

← Back to Index