Commit 2024-06-17 11:20 e6faccc1

View on Github →

chore(NumberTheory/MulChar): deprecate IsNontrivial, fix isPrimitive (#13878)

  • Deprecate MulChar.IsNontrivial (following the analogous change for AddChar's a few days ago);
  • fix capitalisation of DirichletCharacter.isPrimitive;
  • adjust some lemmas to take a Nat argument with a NeZero instance, rather than a PNat, which is more general and flexible.

Estimated changes

modified theorem gaussSum_sq
modified def AddChar.zmodChar
modified theorem AddChar.zmodChar_apply'
modified theorem AddChar.zmodChar_apply
modified theorem quadraticChar_isNontrivial
added theorem quadraticChar_ne_one
added theorem MulChar.eq_one_iff
added theorem MulChar.ne_one_iff