Def Fin.instAddMonoidWithOne

Modification history

2025-06-06 04:20

Mathlib/Algebra/Group/Fin/Basic.lean

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

Added Fin.instAddMonoidWithOne View on Github →