Commit 2023-01-30 19:17 e6cffe7e

View on Github →

feat: port GroupTheory.Subgroup.Finite (#1864) Zulip thread for the issues I encountered.

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subgroup/Finite.lean

added theorem Subgroup.card_bot

added theorem Subgroup.card_le_one_iff_eq_bot

added theorem Subgroup.eq_bot_of_card_eq

added theorem Subgroup.eq_bot_of_card_le

added theorem Subgroup.eq_top_of_card_eq

added theorem Subgroup.eq_top_of_le_card

added theorem Subgroup.mem_normalizer_fintype

added theorem Subgroup.multiset_noncommProd_mem

added theorem Subgroup.noncommProd_mem

added theorem Subgroup.one_lt_card_iff_ne_bot

added theorem Subgroup.pi_le_iff

added theorem Subgroup.pi_mem_of_mulSingle_mem

added theorem Subgroup.pi_mem_of_mulSingle_mem_aux

added theorem Subgroup.val_finset_prod

added theorem Subgroup.val_list_prod

added theorem Subgroup.val_multiset_prod