cast_add — Mathlib

English

The cast of 1 from ZMod n to R is 1 (simp).

Русский

Образ единицы через приведение равен единице (simp).

LaTeX

$$$\\\\forall {n : \\\\mathbb{N}} {R : Type*} [Ring R] [CharP R n], (ZMod.cast 1) : R = 1$$$

Lean4

@[simp]
theorem cast_add (h : m ∣ n) (a b : ZMod n) : (cast (a + b : ZMod n) : R) = cast a + cast b :=
  by
  cases n
  · apply Int.cast_add
  symm
  dsimp [ZMod, ZMod.cast, ZMod.val]
  rw [← Nat.cast_add, Fin.val_add, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _), @CharP.cast_eq_zero_iff R _ m]
  exact h.trans (Nat.dvd_sub_mod _)

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