map_teichmuller — Mathlib

English

If f is a RingHom, then map f (teichmuller p r) = teichmuller p (f r).

Русский

Пусть f — кольцеобразный гомоморфизм. Тогда map f (teichmuller p r) = teichmuller p (f r).

LaTeX

$$$\\mathrm{map}\; f\\; (\\mathrm{teichmuller}\\ p\\; r) = \\mathrm{teichmuller}\\ p\\; (f r)$$$

Lean4

/-- `teichmuller` is a natural transformation. -/
@[simp]
theorem map_teichmuller (f : R →+* S) (r : R) : map f (teichmuller p r) = teichmuller p (f r) :=
  map_teichmullerFun _ _ _

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