Commit 2023-12-04 12:41 7d9d044e

View on Github →

fix(NumberTheory/LegendreSymbol/AddCharacter): Disentangle coercion mess for AddChar (#8803) There are two things going on here:

  • AddChar G R has two syntactically different coercions to function G → R:
    • FunLike.coe via AddChar.monoidHomClass
    • AddChar.toFun via AddChar.hasCoeToFun
  • AddChar.hasCoeToFun and AddChar.monoidHomClass together create a diamond for the typeclass problem FunLike (AddChar G R) _ _ This PR fixes both problems by
  • removing the HasCoeToFun instance and the corresponding AddChar.toFun
  • changing MonoidHomClass (AddChar G R) (Multiplicative G) R to FunLike (AddChar G R) G fun _ ↦ R (isn't the whole point of AddChar to go from an additive group to a multiplicative one anyway?) This PR isn't meant to be perfect. It is a stopgag to an issue that has completely startled progress on LeanAPAP. Once it is fixed, a much more thorough refactor will follow. This breaks a rewrite downstream that now unifies to some defeq but not syntactically equal type. This is more an indication of fragility in the original proof.

Estimated changes

deleted def AddChar.toFun