cast_one — Mathlib

English

If m divides n, then the image of 1 under ZMod cast to R is equal to 1.

Русский

Если m делит n, то образ единицы через ZMod.cast в R равен 1.

LaTeX

$$$\\\\forall h : m \\\\mid n, \\\\operatorname{cast} (1 : ZMod n) : R = 1$$$

Lean4

@[simp]
theorem cast_one (h : m ∣ n) : (cast (1 : ZMod n) : R) = 1 :=
  by
  rcases n with - | n
  · exact Int.cast_one
  change ((1 % (n + 1) : ℕ) : R) = 1
  cases n
  · rw [Nat.dvd_one] at h
    subst m
    subsingleton [CharP.CharOne.subsingleton]
  rw [Nat.mod_eq_of_lt]
  · exact Nat.cast_one
  exact Nat.lt_of_sub_eq_succ rfl

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