smul

Mathlib.RingTheory.Ideal.Over

URI: https://scilib.ai/kg/mathlib#Ideal.LiesOver.smul

English

If P lies over p, then the g‑twisted ideal g·P lies over p for any g ∈ G.

Русский

Если P лежит над p, то для любого g ∈ G идеал g·P лежит над p.

LaTeX

$$$ P.LiesOver p \\Rightarrow (g \\cdot P).LiesOver p. $$$

Lean4

instance smul [h : P.LiesOver p] : (g • P).LiesOver p :=
  ⟨h.over.trans (under_smul A P g).symm⟩

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

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

Разделы

Аффилиация

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