instIsScalarTowerResidueField — Mathlib

English

For a basis b of S, the i-th element of the quotient basis is the image of b_i under the quotient map to S/pS.

Русский

Для базиса b множества S, i-й элемент базиса в S/pS равен образу b_i по отношению к фактор-модулю.

LaTeX

$$$(basisQuotient\\, b)\\, i = \\mathrm{Ideal.Quotient.mk} \\; p_S \\ (b\\, i)$$$

Lean4

instance {R₁ R₂} [CommRing R₁] [CommRing R₂] [Algebra R₁ R₂] [Algebra R₁ R] [Algebra R₂ R] [IsScalarTower R₁ R₂ R] :
    IsScalarTower R₁ R₂ (IsLocalRing.ResidueField R) := by delta IsLocalRing.ResidueField; infer_instance

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