lift_self — Mathlib

English

The lifting map applied to an element z ∈ ℤ_[p] is the identity, i.e., lift zmod_cast_comp_toZModPow z = z.

Русский

Возведение подстановки к элементу z ∈ ℤ_[p] даёт сам z: lift zmod_cast_comp_toZModPow z = z.

LaTeX

$$$\\text{lift} \\ z_{\\text{mod\\_cast\\_comp\\_toZModPow}}(z) = z$$$

Lean4

@[simp]
theorem lift_self (z : ℤ_[p]) : lift zmod_cast_comp_toZModPow z = z :=
  by
  change _ = RingHom.id _ z
  rw [lift_unique zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])]
  intro; rw [RingHom.comp_id]

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