Saturated

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

Statistics

Metric	Count
Definitions Saturated, Saturated	2
Theorems ker_saturated, saturated_iff_nsmul, saturated_iff_zsmul, saturated_iff_npow, saturated_iff_zpow	5
Total	7

AddSubgroup

Definitions

Name	Category	Theorems
Saturated 📖	MathDef	3 math math: saturated_iff_zsmul, saturated_iff_nsmul, ker_saturated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_saturated 📖	mathematical	—	Saturated AddMonoidHom.ker AddMonoid.toAddZeroClass	—	map_nsmul AddMonoidHom.instAddMonoidHomClass
saturated_iff_nsmul 📖	mathematical	—	Saturated AddSubgroup SetLike.instMembership instSetLike	—	—
saturated_iff_zsmul 📖	mathematical	—	Saturated AddSubgroup SetLike.instMembership instSetLike	—	natCast_zsmul negSucc_zsmul neg_mem_iff AddSubgroupClass.toNegMemClass instAddSubgroupClass IsEmpty.forall_iff instIsEmptyFalse

Subgroup

Definitions

Name	Category	Theorems
Saturated 📖	MathDef	2 math math: saturated_iff_zpow, saturated_iff_npow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
saturated_iff_npow 📖	mathematical	—	Saturated Subgroup SetLike.instMembership instSetLike	—	—
saturated_iff_zpow 📖	mathematical	—	Saturated Subgroup SetLike.instMembership instSetLike	—	zpow_natCast zpow_negSucc SubgroupClass.toInvMemClass instSubgroupClass instIsEmptyFalse

---

← Back to Index