Documentation Verification Report

Ideal

📁 Source: Mathlib/Algebra/Group/Ideal.lean

Statistics

Metric	Count
Definitions `AddSemigroupIdeal`, `closure`, `SemigroupIdeal`, `closure`	4
Theorems `add_mem`, `closure_le`, `closure_mono`, `coe_closure`, `coe_closure'`, `fg_iff`, `mem_closure`, `mem_closure'`, `mem_closure''`, `mem_closure_of_mem`, `subset_closure`, `closure_le`, `closure_mono`, `coe_closure`, `coe_closure'`, `fg_iff`, `mem_closure`, `mem_closure'`, `mem_closure''`, `mem_closure_of_mem`, `mul_mem`, `subset_closure`	22
Total	26

AddSemigroupIdeal

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	10 math math: `mem_closure`, `subset_closure`, `closure_le`, `coe_closure`, `coe_closure'`, `mem_closure''`, `mem_closure_of_mem`, `mem_closure'`, `closure_mono`, `fg_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem` 📖	—	`AddSemigroupIdeal` `SetLike.instMembership` `SubAddAction.instSetLike` `Add.toVAdd`	—	—	`SubAddAction.vadd_mem`
`closure_le` 📖	mathematical	—	`AddSemigroupIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `SubAddAction.instPartialOrder` `Add.toVAdd` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `SubAddAction.instSetLike`	—	`SubAddAction.closure_le`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`AddSemigroupIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `SubAddAction.instPartialOrder` `Add.toVAdd` `closure`	—	`SubAddAction.closure_mono`
`coe_closure` 📖	mathematical	—	`SetLike.coe` `AddSemigroupIdeal` `AddSemigroup.toAdd` `SubAddAction.instSetLike` `Add.toVAdd` `closure` `Set` `Set.instUnion` `Set.add` `Set.univ`	—	`Set.add_mem_add` `Set.mem_univ` `add_assoc` `Set.mem_union` `LE.le.antisymm` `closure_le` `mem_closure_of_mem` `add_mem`
`coe_closure'` 📖	mathematical	—	`SetLike.coe` `AddSemigroupIdeal` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubAddAction.instSetLike` `Add.toVAdd` `closure` `Set` `Set.add` `Set.univ`	—	`coe_closure` `Set.union_eq_right` `Set.mem_univ` `zero_add`
`fg_iff` 📖	mathematical	—	`FG` `closure` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`SubAddAction.fg_iff`
`mem_closure` 📖	mathematical	—	`AddSemigroupIdeal` `SetLike.instMembership` `SubAddAction.instSetLike` `Add.toVAdd` `closure`	—	`SubAddAction.mem_closure`
`mem_closure'` 📖	mathematical	—	`AddSemigroupIdeal` `AddSemigroup.toAdd` `SetLike.instMembership` `SubAddAction.instSetLike` `Add.toVAdd` `closure` `Set` `Set.instMembership`	—	`SetLike.mem_coe` `coe_closure` `Set.mem_union` `Set.mem_add` `Set.mem_univ`
`mem_closure''` 📖	mathematical	—	`AddSemigroupIdeal` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `SubAddAction.instSetLike` `Add.toVAdd` `closure` `Set` `Set.instMembership`	—	`SetLike.mem_coe` `coe_closure'` `Set.mem_add` `Set.mem_univ`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`AddSemigroupIdeal` `SetLike.instMembership` `SubAddAction.instSetLike` `Add.toVAdd` `closure`	—	`SubAddAction.mem_closure_of_mem`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `AddSemigroupIdeal` `SubAddAction.instSetLike` `Add.toVAdd` `closure`	—	`SubAddAction.subset_closure`

SemigroupIdeal

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	10 math math: `fg_iff`, `mem_closure''`, `subset_closure`, `coe_closure`, `closure_le`, `mem_closure`, `mem_closure_of_mem`, `coe_closure'`, `closure_mono`, `mem_closure'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_le` 📖	mathematical	—	`SemigroupIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `SubMulAction.instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `SubMulAction.instSetLike`	—	`SubMulAction.closure_le`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`SemigroupIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `SubMulAction.instPartialOrder` `closure`	—	`SubMulAction.closure_mono`
`coe_closure` 📖	mathematical	—	`SetLike.coe` `SemigroupIdeal` `Semigroup.toMul` `SubMulAction.instSetLike` `closure` `Set` `Set.instUnion` `Set.mul` `Set.univ`	—	`Set.mul_mem_mul` `Set.mem_univ` `LE.le.antisymm` `closure_le` `mem_closure_of_mem` `mul_mem`
`coe_closure'` 📖	mathematical	—	`SetLike.coe` `SemigroupIdeal` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SubMulAction.instSetLike` `closure` `Set` `Set.mul` `Set.univ`	—	`coe_closure` `Set.union_eq_right` `Set.mem_univ` `one_mul`
`fg_iff` 📖	mathematical	—	`FG` `closure` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`SubMulAction.fg_iff`
`mem_closure` 📖	mathematical	—	`SemigroupIdeal` `SetLike.instMembership` `SubMulAction.instSetLike` `closure`	—	`SubMulAction.mem_closure`
`mem_closure'` 📖	mathematical	—	`SemigroupIdeal` `Semigroup.toMul` `SetLike.instMembership` `SubMulAction.instSetLike` `closure` `Set` `Set.instMembership`	—	`SetLike.mem_coe` `coe_closure`
`mem_closure''` 📖	mathematical	—	`SemigroupIdeal` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SetLike.instMembership` `SubMulAction.instSetLike` `closure` `Set` `Set.instMembership`	—	`SetLike.mem_coe` `coe_closure'`
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`SemigroupIdeal` `SetLike.instMembership` `SubMulAction.instSetLike` `closure`	—	`SubMulAction.mem_closure_of_mem`
`mul_mem` 📖	—	`SemigroupIdeal` `SetLike.instMembership` `SubMulAction.instSetLike`	—	—	`SubMulAction.smul_mem`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `SemigroupIdeal` `SubMulAction.instSetLike` `closure`	—	`SubMulAction.subset_closure`

(root)

Definitions

Name	Category	Theorems
`AddSemigroupIdeal` 📖	CompOp	10 math math: `AddSemigroupIdeal.mem_closure`, `AddSemigroupIdeal.subset_closure`, `AddSemigroupIdeal.closure_le`, `AddSemigroupIdeal.coe_closure`, `AddSemigroupIdeal.coe_closure'`, `AddSemigroupIdeal.mem_closure''`, `AddSemigroupIdeal.instWellFoundedGT`, `AddSemigroupIdeal.mem_closure_of_mem`, `AddSemigroupIdeal.mem_closure'`, `AddSemigroupIdeal.closure_mono`
`SemigroupIdeal` 📖	CompOp	10 math math: `SemigroupIdeal.mem_closure''`, `SemigroupIdeal.subset_closure`, `SemigroupIdeal.instWellFoundedGT`, `SemigroupIdeal.coe_closure`, `SemigroupIdeal.closure_le`, `SemigroupIdeal.mem_closure`, `SemigroupIdeal.mem_closure_of_mem`, `SemigroupIdeal.coe_closure'`, `SemigroupIdeal.closure_mono`, `SemigroupIdeal.mem_closure'`

---

← Back to Index