diffToIdealOfQuotientCompEq_apply

English

For f1, f2 as above and e witnessing their equality after quotient, the value of the linear map diffToIdealOfQuotientCompEq on x equals f1(x) − f2(x) in B.

Русский

Для отображения diffToIdealOfQuotientCompEq, примененного к x, получаем значение f1(x) − f2(x) в B.

LaTeX

$$$((diffToIdealOfQuotientCompEq I f1 f2 e) x : B) = f1 x - f2 x$$$

Lean4

@[simp]
theorem diffToIdealOfQuotientCompEq_apply (f₁ f₂ : A →ₐ[R] B)
    (e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂) (x : A) :
    ((diffToIdealOfQuotientCompEq I f₁ f₂ e) x : B) = f₁ x - f₂ x :=
  rfl

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