Commit 2026-08-11 11:20 d0eb2622

View on Github →

chore: fix all instances of linter.defProp (#42463) I've omitted the MathlibTest folder, since it's a bit difficult to tell which of those usages are intended.

Estimated changes

Modified Mathlib/CategoryTheory/Category/Preorder.lean

Modified Mathlib/Combinatorics/Hindman.lean

added theorem Hindman.FP.cons

added theorem Hindman.FP.head

added theorem Hindman.FP.tail

Modified Mathlib/Computability/Partrec.lean

Modified Mathlib/Computability/Primrec/Basic.lean

Modified Mathlib/Data/Nat/Find.lean

Modified Mathlib/NumberTheory/Padics/Hensel.lean