Commit 2025-10-20 11:16 fa41ffec

View on Github →

chore: backport grind annotation changes from nightly-testing (#30572)

Estimated changes

Modified Mathlib/Algebra/Group/Units/Defs.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

modified theorem CFC.log_one

modified theorem CFC.log_zero

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

Modified Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

Modified Mathlib/Data/Finset/Attach.lean

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/Finset/Empty.lean

Modified Mathlib/Data/Fintype/Defs.lean

Modified Mathlib/Data/List/Triplewise.lean

Modified Mathlib/Data/Multiset/ZeroCons.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/Insert.lean

Modified Mathlib/Data/Set/Operations.lean

Modified Mathlib/Order/CompleteLattice/MulticoequalizerDiagram.lean

Modified MathlibTest/Simps.lean

Modified MathlibTest/grind/pairwise_disjoint.lean