English
The two ways of viewing the scalar map from S into the quotient agree: the image of s under the algebra map to the quotient equals the quotient of the image of s under the original algebra map to A.
Русский
Две трактовки отображения скаляра s из S в фактор-объект совпадают: образ s в фактор-пространстве через алгебраическое отображение совпадает с образом s через алгебраическое отображение в A, затем взятым по равносильной эквивалентности факторизации.
LaTeX
$$$(\\mathrm{algebraMap}\\; S\\; A\\ s : c.Quotient) = \\mathrm{algebraMap}\\; S\\; c.Quotient\\ s.$$$
Lean4
@[simp, norm_cast]
theorem coe_algebraMap (c : RingCon A) (s : S) : (algebraMap S A s : c.Quotient) = algebraMap S _ s :=
rfl
