finEquiv — Mathlib

English

For every nonzero n, Fin n is ring-equivalent to ZMod n (Fin n ≃+* ZMod n).

Русский

Для любого ненулевого n имеется кольцевое эквивалентство Fin n и ZMod n: Fin n ≃+* ZMod n.

LaTeX

$$$ \forall n,\; [\mathrm{NeZero}\ n] \Rightarrow \mathrm{Fin}\ n \simeq_{+*} \mathrm{ZMod}\ n$$$

Lean4

/-- For non-zero `n : ℕ`, the ring `Fin n` is equivalent to `ZMod n`. -/
def finEquiv : ∀ (n : ℕ) [NeZero n], Fin n ≃+* ZMod n
  | 0, h => (h.ne _ rfl).elim
  | _ + 1, _ => .refl _

Похожие утверждения