Prufer

Statistics

Metric	Count
Definitions	0
Theorems `smul_eq_self_of_preimage_zpow_eq_self`, `vadd_eq_self_of_preimage_zsmul_eq_self`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_eq_self_of_preimage_zpow_eq_self` 📖	mathematical	`Set.preimage` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`Function.IsFixedPt.preimage_iterate` `zpow_iterate` `iterate_map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `one_mul` `le_antisymm` `smul_inv_smul` `inv_zpow` `inv_one`
`vadd_eq_self_of_preimage_zsmul_eq_self` 📖	mathematical	`Set.preimage` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`Function.IsFixedPt.preimage_iterate` `zsmul_iterate` `iterate_map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `zero_add` `le_antisymm` `vadd_neg_vadd` `zsmul_neg` `neg_zero` `Set.vadd_set_subset_vadd_set_iff`

---