ofSubsemiring — Mathlib

English

An algebra over R induces an algebra structure over a subsemiring S, using the composed algebraMap with the inclusion S → R.

Русский

Алгебра над R порождает структуру S-алгебры на A через композицию S ↪ R и исходного отображения R → A.

LaTeX

$$Algebra S A$$

Lean4

/-- Algebra over a subsemiring. This builds upon `Subsemiring.module`. -/
instance ofSubsemiring (S : Subsemiring 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

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