English
For n with NeZero n, Fin(n) has a canonical AddMonoidWithOne structure, with natCast given by Fin.ofNat n.
Русский
Для n, такого что n ≠ 0, Fin(n) имеет каноническую структуру AddMonoidWithOne, где отображение natCast задаётся через Fin.ofNat n.
LaTeX
$$$\\mathrm{AddMonoidWithOne}(\\mathrm{Fin}(n))\\quad(\\text{with } n\\neq 0)$$$
Lean4
/-- This is not a global instance, but can introduced locally using `open Fin.NatCast in ...`.
This is not an instance because the `binop%` elaborator assumes that
there are no non-trivial coercion loops,
but this instance would introduce a coercion from `Nat` to `Fin n` and back.
Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.
For example, for `x : Fin k` and `n : Nat`,
it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
silently introducing wraparound arithmetic.
-/
def instAddMonoidWithOne (n) [NeZero n] : AddMonoidWithOne (Fin n)
where
__ := inferInstanceAs (AddCommMonoid (Fin n))
natCast i := Fin.ofNat n i
natCast_zero := rfl
natCast_succ _ := Fin.ext (add_mod _ _ _)
