lift_castAddHom — Mathlib

English

For x ∈ ℤ, lift n f (Int.castAddHom (ZMod n) x) equals f.1 x, i.e., the lift agrees with the underlying integer hom.

Русский

Для x ∈ ℤ, lift n f (Int.castAddHom (ZMod n) x) совпадает с f.1 x; то есть поднятие согласуется с исходным целочисленным гомоморфизмом.

LaTeX

$$$\mathrm{lift}\ n\ f (\mathrm{Int.castAddHom}(\mathrm{ZMod}\ n)\ x) = f.1 x$$$

Lean4

theorem lift_castAddHom (x : ℤ) : lift n f (Int.castAddHom (ZMod n) x) = f.1 x :=
  AddMonoidHom.liftOfRightInverse_comp_apply _ _ (fun _ => intCast_zmod_cast _) _ _

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