Documentation Verification Report

Saturated

📁 Source: Mathlib/GroupTheory/Subgroup/Saturated.lean

Statistics

Metric	Count
Definitions `Saturated`, `NSMulSaturated`, `Saturated`, `PowSaturated`	4
Theorems `ker_saturated`, `saturated_iff_nsmul`, `saturated_iff_zsmul`, `ker_saturated`, `nsmulSaturated_iff_nsmul`, `saturated_iff_npow`, `saturated_iff_zpow`, `powSaturated_iff_npow`	8
Total	12

AddSubgroup

Definitions

Name	Category	Theorems
`Saturated` 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_saturated` 📖	mathematical	—	`AddSubmonoid.NSMulSaturated` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSubmonoid` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass`	—	`AddSubmonoid.ker_saturated`
`saturated_iff_nsmul` 📖	mathematical	—	`AddSubmonoid.NSMulSaturated` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike`	—	`AddSubmonoid.nsmulSaturated_iff_nsmul`
`saturated_iff_zsmul` 📖	mathematical	—	`AddSubmonoid.NSMulSaturated` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSubmonoid` `AddSubgroup` `SetLike.instMembership` `instSetLike`	—	`mem_toAddSubmonoid` `natCast_zsmul` `neg_zsmul` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass`

AddSubmonoid

Definitions

Name	Category	Theorems
`NSMulSaturated` 📖	MathDef	5 math math: `nsmulSaturated_iff_nsmul`, `AddSubgroup.saturated_iff_zsmul`, `AddSubgroup.saturated_iff_nsmul`, `ker_saturated`, `AddSubgroup.ker_saturated`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_saturated` 📖	mathematical	—	`NSMulSaturated` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddSubmonoid` `AddMonoidHom.ker` `AddMonoid.toAddZeroClass`	—	`AddMonoidHom.instAddMonoidHomClass` `map_nsmul`
`nsmulSaturated_iff_nsmul` 📖	mathematical	—	`NSMulSaturated` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike`	—	—

Subgroup

Definitions

Name	Category	Theorems
`Saturated` 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`saturated_iff_npow` 📖	mathematical	—	`Submonoid.PowSaturated` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike`	—	`Submonoid.powSaturated_iff_npow`
`saturated_iff_zpow` 📖	mathematical	—	`Submonoid.PowSaturated` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSubmonoid` `Subgroup` `SetLike.instMembership` `instSetLike`	—	`zpow_natCast` `zpow_neg` `SubgroupClass.toInvMemClass` `instSubgroupClass`

Submonoid

Definitions

Name	Category	Theorems
`PowSaturated` 📖	MathDef	3 math math: `Subgroup.saturated_iff_zpow`, `powSaturated_iff_npow`, `Subgroup.saturated_iff_npow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`powSaturated_iff_npow` 📖	mathematical	—	`PowSaturated` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike`	—	—

---

← Back to Index