val_unit' — Mathlib

English

In ZMod 0, an element n is a unit if and only if its representative is 1: IsUnit n ↔ n.val = 1.

Русский

В ZMod 0 элемент является единицей тогда и только тогда, когда его представление равно 1: IsUnit n ⇔ n.val = 1.

LaTeX

$$$ \mathrm{IsUnit}(n) \iff n.\mathrm{val} = 1 $$$

Lean4

theorem val_unit' {n : ZMod 0} : IsUnit n ↔ n.val = 1 :=
  by
  simp only [val]
  rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]

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