Basic

Statistics

Metric	Count
Definitions	0
Theorems `dvd_sub_pow_of_dvd_sub`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_sub_pow_of_dvd_sub` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Nat.instMonoid`	—	`pow_one` `pow_zero` `pow_succ` `pow_mul` `geom_sum₂_mul` `pow_succ'` `mul_dvd_mul` `Ideal.instIsTwoSided_1` `Ideal.Quotient.eq_zero_iff_mem` `Ideal.mem_span_singleton` `RingHom.map_geom_sum₂` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `sub_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `geom_sum₂_self` `mul_eq_zero_of_left` `map_natCast` `dvd_refl`

---