cast_eq_mod

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#CharP.cast_eq_mod

← MathLib Explorer

English

For any k, (k : R) = (k mod p) in R.

Русский

Для любого k: (k : R) = (k mod p) в R.

LaTeX

$$$(k : R) = (k \bmod p : \mathbb{N})$$$

Lean4

theorem cast_eq_mod (k : ℕ) : (k : R) = (k % p : ℕ) :=
  have (a : ℕ) : ((p * a : ℕ) : R) = 0 := by
    rw [CharP.cast_eq_zero_iff R p]
    exact Nat.dvd_mul_right p a
  calc
    (k : R) = ↑(k % p + p * (k / p)) := by rw [Nat.mod_add_div]
    _ = ↑(k % p) := by simp [this]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru