Commit 2025-11-12 10:34 85eb1496

View on Github →

refactor: redefine Equiv.Set.sumCompl = Equiv.sumCompl (#30890)

Estimated changes

Modified Mathlib/Logic/Equiv/Set.lean

modified theorem Equiv.Set.sumCompl_symm_apply

Modified Mathlib/Logic/Equiv/Sum.lean