WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Divisor

Revision #2257 → #2900 · back to history

modifiedDivisors from prime factorization5b23ef85b765
FieldFrom #2257To #2900
note`Nat.divisors_prime_pow` and `Nat.mem_divisors_prime_pow` characterize divisors via prime factorization; the general statement follows from `isMultiplicative_sigma`.`Nat.divisors_prime_pow` and `Nat.mem_divisors_prime_pow` characterize divisors via prime factorization; the general statement follows from `Nat.factorization` together with `UniqueFactorizationMonoid`.
addedMultiple of an integer99c0e69b7739
addedNot-a-divisor notatione225bd043507
addedAntisymmetry of divisibility up to units1fbca9754326
addedComplete distributive lattice of divisibility0f5eb40af616