zmodRepr_natCast_of_lt

Mathlib.NumberTheory.Padics.RingHoms

URI: https://scilib.ai/kg/mathlib#PadicInt.zmodRepr_natCast_of_lt

English

zmodRepr of a natural less than p equals the natural itself.

Русский

zmodRepr(nat<n) = nat, если nat < p.

LaTeX

$$∀ {n : ℕ}, n < p → zmodRepr (n : ℤ_[p]) = n$$

Lean4

theorem zmodRepr_natCast_of_lt {n : ℕ} (hn : n < p) : zmodRepr (n : ℤ_[p]) = n := by
  rw [zmodRepr_natCast (p := p) n, Nat.mod_eq_of_lt hn]

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

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

Разделы

Аффилиация

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