zmodEquivTrunc_apply — Mathlib

English

For x in ZMod(p^n), zmodEquivTrunc p n sends x to ZMod.castHom (m := p^n) (proof) (TruncatedWittVector p n (ZMod p)) x.

Русский

Для x ∈ ZMod(p^n) отображение zmodEquivTrunc p n отправляет x в ZMod.castHom (m := p^n) (доказательство) (TruncatedWittVector p n (ZMod p)) x.

LaTeX

$$$$ zmodEquivTrunc(p,n)(x) = ZMod.castHom (m := p^n) (by rfl) ( \mathrm{TruncatedWittVector}_p^n(\mathbb{Z}/p\mathbb{Z}) )(x). $$$$

Lean4

theorem zmodEquivTrunc_apply {x : ZMod (p ^ n)} :
    zmodEquivTrunc p n x = ZMod.castHom (m := p ^ n) (by rfl) (TruncatedWittVector p n (ZMod p)) x :=
  rfl

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