instAlgebraQuotient — Mathlib

English

If A carries compatible R1- and R2-algebra structures with a scalar tower, then the quotient A/I also inherits a compatible IsScalarTower structure from R1 and R2.

Русский

Если A обладает совместимыми структурами R1- и R2-алгебр и существует тензорная башня скаляров, то частное A/I тоже наследует совместимую структуру IsScalarTower от R1 и R2.

LaTeX

$$$ \text{IsScalarTower } R_1 R_2 (A/I) $$$

Lean4

instance {A} [CommRing A] [Algebra R₁ A] (I : Ideal A) : Algebra R₁ (A ⧸ I) :=
  inferInstance

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