Commit 2024-06-14 14:02 239c8221

View on Github →

feat(AddChar): Various improvements (#13579)

  • Add a bunch of missing simp and norm_cast lemmas.
  • Get rid of IsNontrivial ψ since it's just ψ ≠ 1. This simplifies proofs.
  • Remove explicit arguments to toMonoidHomEquiv/toAddMonoidHomEquiv. We basically never need to provide them explicitly since unification usually does the job.

Estimated changes

added theorem AddChar.coe_mul
added theorem AddChar.coe_one
added theorem AddChar.coe_pow
added theorem AddChar.eq_one_iff
added theorem AddChar.injective_iff
added theorem AddChar.map_sub_eq_div
modified theorem AddChar.mul_apply
added theorem AddChar.ne_one_iff
modified theorem AddChar.pow_apply
modified theorem gaussSum_sq
modified def AddChar.IsPrimitive