lift_coe — Mathlib

English

For x ∈ ℤ, the evaluation of the lifted map at x coincides with f.val x, i.e., lift n f (x) = f.val x.

Русский

Для x ∈ ℤ, значение поднятого отображения в точке x совпадает с f.val x; то есть lift n f (x) = f.val x.

LaTeX

$$$\mathrm{lift}\ n\ f\ (x) = f.\mathrm{val}\ x$$$

Lean4

@[simp]
theorem lift_coe (x : ℤ) : lift n f (x : ZMod n) = f.val x :=
  AddMonoidHom.liftOfRightInverse_comp_apply _ _ (fun _ => intCast_zmod_cast _) _ _

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