Commit 2023-09-28 15:48 42019ce8

View on Github →

feat: add theorem cast_subgroup_of_units_card_ne_zero (#6500) Adds a theorem saying the cardinality of a multiplicative subgroup of a field, cast to the field, is nonzero. As well as sum_subgroup_units_zero_of_ne_bot and other theorems about summing over multiplicative subgroups.

Estimated changes

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Multiset.map_univ_val_equiv

Modified Mathlib/FieldTheory/Finite/Basic.lean

added theorem FiniteField.card_cast_subgroup_card_ne_zero

added theorem FiniteField.sum_subgroup_pow_eq_zero

added theorem FiniteField.sum_subgroup_units

added theorem FiniteField.sum_subgroup_units_eq_zero

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem card_zpowers_le

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

added theorem exists_pow_ne_one_of_isCyclic

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem Subgroup.exists_ne_one_of_nontrivial

added theorem Subgroup.ne_bot_iff_exists_ne_one

added theorem Subgroup.nontrivial_iff_ne_bot