mkₐ_toRingHom — Mathlib

English

The underlying ring homomorphism of mkₐ f is the same as mk f, i.e., the algebra-valued quotient map agrees with the plain ring quotient map on the underlying ring structure.

Русский

Основное кольцо отображение mkₐ f совпадает с mk f на уровне кольца: отображение фактор-модуля согласуется.

LaTeX

$$$\\uparrow mk_\\!a_f = mk_f$$$

Lean4

@[simp, norm_cast]
theorem mkₐ_toRingHom : ↑(mkₐ f) = mk f :=
  rfl

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