Documentation Verification Report

Divisibility

📁 Source: Mathlib/SetTheory/Cardinal/Divisibility.lean

Statistics

Metric	Count
Definitions `instUniqueUnits`	1
Theorems `dvd_of_le_of_aleph0_le`, `isPrimePow_iff`, `isUnit_iff`, `is_prime_iff`, `le_of_dvd`, `nat_coe_dvd_iff`, `nat_is_prime_iff`, `not_irreducible_of_aleph0_le`, `prime_of_aleph0_le`	9
Total	10

Cardinal

Definitions

Name	Category	Theorems
`instUniqueUnits` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_of_le_of_aleph0_le` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	—	`mul_eq_right`
`isPrimePow_iff` 📖	mathematical	—	`IsPrimePow` `Cardinal` `instCommMonoidWithZero` `instLE` `aleph0` `instNatCast` `Nat.instCommMonoidWithZero`	—	`Prime.isPrimePow` `prime_of_aleph0_le` `CanLift.prf` `canLiftCardinalNat` `not_le` `isPrimePow_def` `power_le_power_left` `Prime.ne_zero` `Nat.cast_one` `addLeftMono` `IsOrderedRing.toZeroLEOneClass` `isOrderedRing` `instCharZero` `LE.le.trans_lt` `power_one` `natCast_lt_aleph0` `nat_is_prime_iff`
`isUnit_iff` 📖	mathematical	—	`IsUnit` `Cardinal` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `instOne`	—	`eq_or_ne` `not_isUnit_zero` `instNontrivial` `isUnit_iff_forall_dvd` `mul_eq_one_iff_of_one_le` `CanonicallyOrderedAdd.toMulLeftMono` `canonicallyOrderedAdd` `covariant_swap_mul_of_covariant_mul` `one_le_iff_ne_zero` `zero_ne_one` `NeZero.charZero_one` `instCharZero` `MulZeroClass.mul_zero` `isUnit_one`
`is_prime_iff` 📖	mathematical	—	`Prime` `Cardinal` `instCommMonoidWithZero` `instLE` `aleph0` `instNatCast` `Nat.Prime`	—	`le_or_gt` `CanLift.prf` `canLiftCardinalNat` `not_le` `instCharZero`
`le_of_dvd` 📖	mathematical	`Cardinal` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	`instLE`	—	`mul_one` `mul_le_mul_right` `CanonicallyOrderedAdd.toMulLeftMono` `canonicallyOrderedAdd` `one_le_iff_ne_zero` `MulZeroClass.mul_zero`
`nat_coe_dvd_iff` 📖	mathematical	—	`Cardinal` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring` `instNatCast`	—	`natCast_lt_aleph0` `mul_lt_aleph0_iff` `MulZeroClass.zero_mul` `instCharZero` `MulZeroClass.mul_zero` `CanLift.prf` `canLiftCardinalNat`
`nat_is_prime_iff` 📖	mathematical	—	`Prime` `Cardinal` `instCommMonoidWithZero` `instNatCast` `Nat.Prime`	—	`instCharZero` `Nat.cast_one` `lt_or_ge` `mul_lt_aleph0_iff` `CanLift.prf` `canLiftCardinalNat` `aleph0_le_mul_iff` `mul_eq_zero` `noZeroDivisors` `zero_dvd_iff` `dvd_of_le_of_aleph0_le` `LE.le.trans` `LT.lt.le` `natCast_lt_aleph0` `mul_comm`
`not_irreducible_of_aleph0_le` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`Irreducible` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring`	—	`irreducible_iff` `not_and_or` `mul_aleph0_eq` `Unique.instSubsingleton` `LT.lt.ne'` `LT.lt.trans_le` `one_lt_aleph0`
`prime_of_aleph0_le` 📖	mathematical	`Cardinal` `instLE` `aleph0`	`Prime` `instCommMonoidWithZero`	—	`LT.lt.ne'` `LT.lt.trans_le` `aleph0_pos` `isUnit_iff` `one_lt_aleph0` `eq_or_ne` `mul_eq_zero` `noZeroDivisors` `le_of_dvd` `max_def'` `mul_eq_max'` `LE.le.trans` `le_total` `mul_comm`

---

← Back to Index