Commit 2023-07-19 11:17 293041f7

View on Github →

feat: add card_units_add_one lemma (#5738) A lemma to reexpress card_units without subtraction.

Estimated changes

Modified Mathlib/Data/Fintype/Units.lean

added theorem Fintype.card_eq_card_units_add_one

modified theorem Fintype.card_units

added theorem Nat.card_eq_card_units_add_one

Modified Mathlib/FieldTheory/Finite/Basic.lean

modified theorem FiniteField.sum_pow_units