Theorem ArithmeticFunction.cardFactors_pos_iff_one_lt

Modification history

2025-12-02 09:01
Mathlib/NumberTheory/ArithmeticFunction.lean
refactor(NumberTheory/ArithmeticFunction): split long file (#32304) …
Modified ArithmeticFunction.cardFactors_pos_iff_one_ltView on Github →
2025-08-27 05:29
Mathlib/NumberTheory/ArithmeticFunction.lean
feat(NumberTheory/ArithmeticFunction): some additional theorems for `cardFactors` (`Ω`) (#28941)
Added ArithmeticFunction.cardFactors_pos_iff_one_ltView on Github →