toAlgebra_algebraMap — Mathlib

English

Let R and S be commutative semirings and S an algebra over R. Then the algebra structure on S induced by the algebra map algebraMap R S coincides with the given Algebra R S structure.

Русский

Пусть R и S — коммутативные полукольца, и S является R-алгеброй. Тогда алгебраическая структура на S, индуцированная отображением algebraMap R S, совпадает с заданной структурой Algebra R S.

LaTeX

$$$(algebraMap\;R\;S).toAlgebra = Algebra\;R\;S$$$

Lean4

/-- An auxiliary lemma used to prove theorems of the form
`RingHom.X (algebraMap R S) ↔ Algebra.X R S`. -/
theorem _root_.toAlgebra_algebraMap [Algebra R S] : (algebraMap R S).toAlgebra = ‹_› :=
  algebra_ext _ _ fun _ ↦ rfl

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