Commit 2024-12-05 08:47 967e4d70

View on Github →

chore(Finset): rename Insert.comm to insert_comm (#19610) and add the DecidablePred Finset.Nontrivial instance. From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/Finset/Insert.lean

deleted theorem Finset.Insert.comm

added theorem Finset.insert_comm

Modified Mathlib/NumberTheory/FLT/Three.lean