Commit 2023-10-12 03:09 644ffced

View on Github →

feat: small missing group lemmas (#7614)

Estimated changes

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem MonoidHom.ker_prod

Modified Mathlib/GroupTheory/Subgroup/Finite.lean

added theorem Subgroup.eq_bot_iff_card

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

added theorem Submonoid.card_bot

added theorem Submonoid.card_le_one_iff_eq_bot

added theorem Submonoid.eq_bot_iff_card

added theorem Submonoid.eq_bot_of_card_eq

added theorem Submonoid.eq_bot_of_card_le

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

added theorem Submonoid.eq_bot_of_subsingleton

Modified Mathlib/GroupTheory/Sylow.lean