coe_rangeRestrict — Mathlib

English

The underlying AlgHom of rangeRestrict equals the AlgHom.rangeRestrict of f.

Русский

Базовый гомоморфизм алгебр из rangeRestrict совпадает с rangeRestrict gомоморфизма f.

LaTeX

$$$\mathrm{toAlgHom}(f\.rangeRestrict) = \mathrm{toAlgHom}(f).rangeRestrict$$$

Lean4

@[simp]
theorem coe_rangeRestrict (f : A →A[R] B) :
    (f.rangeRestrict : A →ₐ[R] (@AlgHom.range R A B _ _ _ _ _ f)) = (f : A →ₐ[R] B).rangeRestrict :=
  rfl

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