Commit 2020-05-12 06:37 295b87ec

View on Github →

feat(ring_theory/integral_domain): sum in integral domain indexed by finite group (#2623) In other words: nontrivial sums are trivial Moved from field_theory.finite to the new ring_theory.integral_domain:

card_nth_roots_subgroup_units
subgroup_units_cyclic

Estimated changes

Modified src/algebra/group/units_hom.lean

added theorem monoid_hom.coe_to_hom_units

added def monoid_hom.to_hom_units

Modified src/data/fintype/card.lean

added theorem finset.prod_subtype

Modified src/field_theory/finite.lean

deleted theorem card_nth_roots_subgroup_units

Modified src/group_theory/order_of_element.lean

added theorem is_cyclic.exists_monoid_generator

Created src/ring_theory/integral_domain.lean

added theorem card_fiber_eq_of_mem_range

added theorem card_nth_roots_subgroup_units

added theorem sum_hom_units

added theorem sum_hom_units_eq_zero