map_equiv_liesOver

Mathlib.RingTheory.Ideal.Over

URI: https://scilib.ai/kg/mathlib#Ideal.map_equiv_liesOver

← MathLib Explorer

English

For any σ, if P lies over p then (P.map σ) lies over p.

Русский

Для любого σ, если P лежит над p, то (P.map σ) лежит над p.

LaTeX

$$$ P.LiesOver p \\Rightarrow (P.map\\, \\sigma).LiesOver p. $$$

Lean4

instance map_equiv_liesOver [P.LiesOver p] {E : Type*} [EquivLike E B C] [AlgEquivClass E A B C] (σ : E) :
    (P.map σ).LiesOver p :=
  LiesOver.of_eq_map_equiv p σ rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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