instAlgebra — Mathlib

English

If A is an R-algebra with a topological semiring, then SeparationQuotient A inherits an algebra structure with a well-defined algebra map and smul.

Русский

Если A — R-алгебра с топологическим полным полем, то SeparationQuotient A наследует структуру алгебры.

LaTeX

$$$\mathrm{Algebra}\ R(\mathrm{SeparationQuotient}A)$$$

Lean4

instance instAlgebra : Algebra R (SeparationQuotient A)
    where
  algebraMap := mkRingHom.comp (algebraMap R A)
  commutes' r := Quotient.ind fun a => congrArg _ <| Algebra.commutes r a
  smul_def' r := Quotient.ind fun a => congrArg _ <| Algebra.smul_def r a

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