Mathlib Changelog
v4
Changelog
About
Github
Theorem
Set.Finite.symmDiff_congr
Modification history
2025-01-10 13:20
Mathlib/Data/Set/Finite/Basic.lean
feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) …
Added
Set.Finite.symmDiff_congr
View on Github →