Def Fin.instCommRing

Modification history

2025-06-07 00:12

Mathlib/Data/ZMod/Defs.lean

fix: restore the `NonUnitalCommRing (Fin n)` instance (#25531) …

Modified Fin.instCommRing View on Github →

2025-06-06 04:20

Mathlib/Data/ZMod/Defs.lean

chore: remove global `NatCast (Fin n)` and `CommRing (Fin n)` instances. (#25476) …

Added Fin.instCommRing View on Github →