ofSubring — Mathlib

English

If S is a subring of R, and A is an algebra over R, then A acquires an S-algebra structure via the inclusion S → R.

Русский

Если S — подп Ring R, а A — алгебра над R, то A получает структуру S-алгебры через включение S → R.

LaTeX

$$Algebra S A$$

Lean4

/-- Algebra over a subring. This builds upon `Subring.module`. -/
instance ofSubring {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (S : Subring R) : Algebra S A
    where
  algebraMap := (algebraMap R A).comp S.subtype
  smul := (· • ·)
  commutes' r x := Algebra.commutes (r : R) x
  smul_def' r x := Algebra.smul_def (r : R) x

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