Commit 2025-12-15 15:28 8b479047

View on Github →

chore: golf using grind. add grind annotations. (#32738)

Estimated changes

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Nat/PrimeFin.lean

modified theorem Nat.mem_primeFactors

Modified Mathlib/Data/Seq/Basic.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/NumberTheory/SumTwoSquares.lean