Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sum_hom_units_eq_zero

Modification history

2020-05-12 06:37
src/ring_theory/integral_domain.lean
feat(ring_theory/integral_domain): sum in integral domain indexed by finite group (#2623) …
Added sum_hom_units_eq_zeroView on Github →