zmodRepr_natCast_ofNat

Mathlib.NumberTheory.Padics.RingHoms

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

← MathLib Explorer

English

If n is a natural with n < p, then zmodRepr(n) = n as an element of ℤ_p.

Русский

Для натурального n с n < p получаем zmodRepr(n) = n в ℤ_p.

LaTeX

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

Lean4

theorem zmodRepr_natCast_ofNat {n : ℕ} (hn : ofNat(n) < p) : zmodRepr (ofNat(n) : ℤ_[p]) = ofNat(n) :=
  by
  convert zmodRepr_natCast_of_lt hn
  rcases n with _ | _ | n <;> simp

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

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

Разделы

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

Аффилиация

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