Lemmas

📁 Source: Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems instCountableSubtypeMemZMultiples, intCast_mem_zmultiples_one, intCast_mul_mem_zmultiples, range_zmultiplesHom, range_castAddHom, instCountableSubtypeMemZpowers, range_zpowersHom	7
Total	7

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountableSubtypeMemZMultiples 📖	mathematical	—	Countable AddSubgroup SetLike.instMembership instSetLike zmultiples	—	Function.Surjective.countable instCountableInt Set.rangeFactorization_surjective
intCast_mem_zmultiples_one 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership instSetLike zmultiples AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toIntCast	—	mem_zmultiples_iff zsmul_eq_mul mul_one
intCast_mul_mem_zmultiples 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership instSetLike zmultiples Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddGroupWithOne.toIntCast	—	zsmul_mem_zmultiples
range_zmultiplesHom 📖	mathematical	—	AddMonoidHom.range Int.instAddGroup DFunLike.coe Equiv AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass Int.instAddMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid EquivLike.toFunLike Equiv.instEquivLike zmultiplesHom zmultiples	—	—

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_castAddHom 📖	mathematical	—	AddMonoidHom.range instAddGroup AddGroupWithOne.toAddGroup castAddHom AddSubgroup.zmultiples AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	AddSubgroup.ext zsmul_one

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountableSubtypeMemZpowers 📖	mathematical	—	Countable Subgroup SetLike.instMembership instSetLike zpowers	—	Function.Surjective.countable instCountableInt Set.rangeFactorization_surjective
range_zpowersHom 📖	mathematical	—	MonoidHom.range Multiplicative Multiplicative.group Int.instAddGroup DFunLike.coe Equiv MonoidHom MulOneClass.toMulOne Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike Equiv.instEquivLike zpowersHom zpowers	—	—

---

← Back to Index