lift_comp_coe — Mathlib

English

The composition of ZMod.lift with the natural embedding of integers into ZMod n is equal to f, i.e., ZMod.lift n f ∘ ((↑) : ℤ → _) = f.

Русский

Сложение ZMod.lift с естественным вложением целых чисел в ZMod n равно f; то есть ZMod.lift n f ∘ (↑) = f.

LaTeX

$$$\mathrm{ZMod}.lift\ n\ f \circ (\uparrow) = f$$$

Lean4

@[simp]
theorem lift_comp_coe : ZMod.lift n f ∘ ((↑) : ℤ → _) = f :=
  funext <| lift_coe _ _

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