coe_sub — Mathlib

English

The inclusion map preserves subtraction: the image of x - y equals the image of x minus the image of y.

Русский

Включение сохраняет разность: образ x - y равен разности образов x и y.

LaTeX

$$$ (x - y)^{\\uparrow} = x^{\\uparrow} - y^{\\uparrow} \\quad (x,y \\in S). $$$

Lean4

protected theorem coe_sub {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A}
    (x y : S) : (↑(x - y) : A) = ↑x - ↑y :=
  rfl

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