Commit 2025-08-08 11:53 f77f5d68

View on Github →

chore(Nat/Factorization/Induction): recursors (#28096) Name the motive motive and name the minor premises according to their constructors. Also clean up Nat.recOnMul.hp''.

Estimated changes

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

modified theorem Nat.prime_composite_induction

modified def Nat.recOnMul

modified def Nat.recOnPosPrimePosCoprime

modified def Nat.recOnPrimeCoprime

modified def Nat.recOnPrimePow

modified theorem induction_on_primes

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/NumberTheory/SumFourSquares.lean

Modified Mathlib/NumberTheory/SumTwoSquares.lean