coe_codRestrict_apply — Mathlib

English

The two ways of viewing the codRestrict construction yield the same underlying algebra homomorphism; equivalently, the two codRestrict constructions agree on maps.

Русский

Два способа задания codRestrict дают одинаковый базовый алгебро-гомоморфизм; эквивалентно, два способа ограничений совпадают на отображениях.

LaTeX

$$$\text{AlgHomClass.toAlgHom}(f\ codRestrict p h) = \text{AlgHomClass.toAlgHom}(f)\ codRestrict p h$$$

Lean4

@[simp]
theorem coe_codRestrict_apply (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x, f x ∈ p) (x) :
    (f.codRestrict p h x : B) = f x :=
  rfl

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