Commit 2024-08-27 16:27 09c79c33

View on Github →

feat: Add/improve lemmas on Set/Subgroup equality (#14365)

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Finite.lean

added theorem Subgroup.card_le_of_le

added theorem Subgroup.eq_of_le_of_card_ge

modified theorem Subgroup.eq_top_of_card_eq

Modified Mathlib/Data/Finite/Card.lean

added theorem Set.eq_top_of_card_le_of_finite