Documentation Verification Report

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`, `range_nsmulAddMonoidHom`, `instCountableSubtypeMemZpowers`, `range_zpowersHom`	8
Total	8

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`
`range_nsmulAddMonoidHom` 📖	mathematical	—	`AddMonoidHom.range` `instAddGroup` `nsmulAddMonoidHom` `instAddCommMonoid` `AddSubgroup.zmultiples`	—	`AddSubgroup.ext`

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