Commit 2024-05-14 23:22 1f4dc050

View on Github →

chore: robustify proofs against leanprover/lean4#4061 (#12906) leanprover/lean4#4061 results in well-founded definitions being irreducible by default. This PR robustifies some proofs. (Sometime over-robust: we're going to keep minFacAux as semireducible for now, so e.g. Nat.Prime 5 will still be decidable.)

Estimated changes

Modified Mathlib/Data/Nat/Choose/Multinomial.lean

modified theorem Multiset.multinomial_zero

Modified Mathlib/Data/Nat/Factorization/Basic.lean

modified theorem Nat.factorization_one

modified theorem Nat.factorization_zero

Modified Mathlib/Data/Nat/Factors.lean

added theorem Nat.factors_two

Modified Mathlib/Data/Nat/Prime.lean

added theorem Nat.minFac_two

Modified Mathlib/Data/Nat/PrimeFin.lean

modified theorem Nat.primeFactors_one

modified theorem Nat.primeFactors_zero

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Data/Sym/Basic.lean

added theorem Sym.toMultiset_zero

Modified Mathlib/GroupTheory/CommutingProbability.lean

modified theorem DihedralGroup.reciprocalFactors_one

modified theorem DihedralGroup.reciprocalFactors_zero

Modified Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean

Modified Mathlib/Tactic/NormNum/Prime.lean