Commit 2024-06-16 15:16 d394d9f4

View on Github →

chore(NumberTheory/MulChar): fix Fintype/Finite, generalize (#13862) In MulChar.orderOf_pos and MulChar.pow_card_eq_one,

  • drop DecidableEq;
  • assume Finite instead of Fintype;
  • only assume finiteness of Mˣ, not M.

Estimated changes

modified theorem MulChar.orderOf_pos
deleted theorem MulChar.pow_card_eq_one