Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-30 18:20 caf93b74

View on Github →

feat(*): small additions that prepare for Chevalley-Warning (#2560) A number a small changes that prepare for #1564.

Estimated changes

Modified src/algebra/associated.lean

deleted theorem is_unit.mk0

deleted theorem is_unit_iff_ne_zero

Modified src/algebra/big_operators.lean

added theorem finset.sum_mul_sum

Modified src/algebra/group_with_zero.lean

added theorem is_unit.mk0

added theorem is_unit_iff_ne_zero

added theorem units.exists_iff_ne_zero

Modified src/data/fintype/basic.lean

added theorem finset.inter_univ

added theorem finset.univ_inter

added theorem set.to_finset_univ

Modified src/data/fintype/card.lean

added theorem fintype.prod_extend_by_one

Modified src/group_theory/order_of_element.lean

added theorem image_range_order_of

added theorem is_cyclic.image_range_card

added theorem is_cyclic.image_range_order_of