toAlgebra — Mathlib

English

There is an algebra structure on α over S obtained by restricting the A-algebra structure along the inclusion S → A.

Русский

Существуют соответствующие алгебраические структуры над S на α, получаемые ограничением структуры над A по включению S → A.

LaTeX

$$$\text{Algebra } S \alpha \text{ is obtained by restricting the } A\text{-algebra structure along } S \hookrightarrow A.$$$

Lean4

/-- The action by a subalgebra is the action by the underlying algebra. -/
instance toAlgebra {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α]
    (S : Subalgebra R A) : Algebra S α :=
  Algebra.ofSubsemiring S.toSubsemiring

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