zmodRepr_natCast_zmodRepr

Mathlib.NumberTheory.Padics.RingHoms

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

← MathLib Explorer

English

zmodRepr(zmodRepr(x)) = zmodRepr(x); applying zmodRepr twice yields the same residual representative.

Русский

zmodRepr(zmodRepr(x)) = zmodRepr(x); повторное применение даёт тот же остаток.

LaTeX

$$zmodRepr(x.zmodRepr) = x.zmodRepr$$

Lean4

@[simp]
theorem zmodRepr_natCast_zmodRepr (x : ℤ_[p]) : (x.zmodRepr : ℤ_[p]).zmodRepr = x.zmodRepr :=
  by
  apply zmodRepr_unique _ _ (zmodRepr_lt_p _)
  simp

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

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

Разделы

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

Аффилиация

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