algebraOfLiesOver

Mathlib.RingTheory.Ideal.Over

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.algebraOfLiesOver

← MathLib Explorer

English

If P lies over p, then B/P carries a natural A/p‑algebra structure.

Русский

Если P лежит над p, то B/P естественным образом является A/p‑алгеброй.

LaTeX

$$$ (A/ p) \\text{-algebra } (B/ P). $$$

Lean4

/-- If `P` lies over `p`, then canonically `B ⧸ P` is a `A ⧸ p`-algebra. -/
instance algebraOfLiesOver : Algebra (A ⧸ p) (B ⧸ P) :=
  algebraQuotientOfLEComap (le_of_eq (P.over_def p))

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

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

Разделы

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

Аффилиация

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