isScalarTower — Mathlib

English

Under the same assumptions as above, the quotient A/I naturally satisfies IsScalarTower R1 R2 (HasQuotient.Quotient A I).

Русский

При тех же предположениях частное A/I естественным образом удовлетворяет IsScalarTower R1 R2 (HasQuotient.Quotient A I).

LaTeX

$$$ \text{IsScalarTower } R_1 R_2 (HasQuotient.Quotient A I) $$$

Lean4

instance isScalarTower [SMul R₁ R₂] [IsScalarTower R₁ R₂ A] (I : Ideal A) : IsScalarTower R₁ R₂ (A ⧸ I) :=
  inferInstance

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