instIsScalarTowerQuotientIdealResidueField

Mathlib.RingTheory.LocalRing.ResidueField.Ideal

URI: https://scilib.ai/kg/mathlib#instIsScalarTowerQuotientIdealResidueField

English

There is a scalar tower R → R/I → I.ResidueField.

Русский

Существует каскад скаляров R → R/I → I.ResidueField.

LaTeX

$$$ \text{IsScalarTower } R \ (R/I)\ I.\mathrm{ResidueField}. $$$

Lean4

instance : IsScalarTower R (R ⧸ I) I.ResidueField :=
  IsScalarTower.of_algebraMap_eq fun _ ↦ rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru