English
For every n with n ≠ 0, the finite type Fin(n) carries a commutative ring structure given by modular arithmetic modulo n.
Русский
Для каждого n, не равного нулю, множество Fin(n) наделяется коммутативным кольцом операций сложения и умножения по модулю n.
LaTeX
$$$\forall n \,(n \neq 0) \Rightarrow Fin(n) \text{ is a commutative ring under the usual mod-}n\text{ arithmetic.}$$$
Lean4
/-- Commutative ring structure on `Fin n`.
This is not a global instance, but can introduced locally using `open Fin.CommRing 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 instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n)
where
__ := Fin.instAddMonoidWithOne n
__ := Fin.addCommGroup n
__ := Fin.instCommSemigroup n
__ := Fin.instNonUnitalCommRing n
__ := Fin.instCommMonoid n
intCast n := Fin.intCast n
