Theorem Nat.factorization_choose_prime_pow

Modification history

2026-10-23 12:20

Mathlib/Data/Nat/Choose/Factorization.lean

feat: `2 ^ n ≤ lcmUpto n` for `7 ≤ n` (#43373) …

Modified Nat.factorization_choose_prime_pow View on Github →

2025-08-09 19:57

Mathlib/Data/Nat/Choose/Factorization.lean

chore: deduce `Nat.multiplicity` lemmas from the `Nat.factorization` ones (#22503) …

Added Nat.factorization_choose_prime_pow View on Github →