nontrivial — Mathlib

English

If n > 1, the ring ZMod n is nontrivial (there exist at least two distinct elements).

Русский

Если n > 1, кольцо ZMod n не тривиально (существуют по меньшей мере два различных элемента).

LaTeX

$$$(1 < n) \Rightarrow \exists a,b : ZMod n, a \neq b$$$

Lean4

instance nontrivial (n : ℕ) [Fact (1 < n)] : Nontrivial (ZMod n) :=
  ⟨⟨0, 1, fun h =>
      zero_ne_one <|
        calc
          0 = (0 : ZMod n).val := by rw [val_zero]
          _ = (1 : ZMod n).val := (congr_arg ZMod.val h)
          _ = 1 := val_one n⟩⟩

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