Theorem Nat.factorization_add_factorization_choose_le_log

Modification history

2026-10-23 12:20
Mathlib/Data/Nat/Choose/Factorization.lean
feat: `2 ^ n ≤ lcmUpto n` for `7 ≤ n` (#43373) …
Added Nat.factorization_add_factorization_choose_le_logView on Github →