cast_neg_one — Mathlib

English

For k ∈ ZMod n, cast(k − 1) equals (if k = 0 then n else cast(k)) − 1.

Русский

Для k ∈ ZMod n, cast(k − 1) равно (если k = 0, то n, иначе cast(k)) − 1.

LaTeX

$$$\operatorname{cast}(k - 1 : \mathbb{Z}/n\mathbb{Z}) = \bigl(\text{if } k = 0 \text{ then } (n : \mathbb{R}) \text{ else cast } k\bigr) - 1$$$

Lean4

/-- `-1 : ZMod n` lifts to `n - 1 : R`. This avoids the characteristic assumption in `cast_neg`. -/
theorem cast_neg_one {R : Type*} [Ring R] (n : ℕ) : cast (-1 : ZMod n) = (n - 1 : R) :=
  by
  rcases n with - | n
  · dsimp [ZMod, ZMod.cast]; simp
  · rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]

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