eval₂Hom_rename — Mathlib

English

For a RingHom f and renaming with k, eval₂Hom f g (rename k p) = eval₂Hom f (g ∘ k) p.

Русский

Для кольцевого гомоморфизма f и переименования k: eval₂Hom f g (rename k p) = eval₂Hom f (g ∘ k) p.

LaTeX

$$$\\mathrm{eval_2Hom} f g (\\text{rename } k\\, p) = \\mathrm{eval_2Hom} f (g \\circ k)\\, p.$$$

Lean4

theorem eval₂Hom_rename : eval₂Hom f g (rename k p) = eval₂Hom f (g ∘ k) p :=
  eval₂_rename _ _ _ _

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