self

Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

URI: https://scilib.ai/kg/mathlib#Module.FaithfullyFlat.self

← MathLib Explorer

English

If p ∈ Spec(A) is prime, there exists a prime P in B with P.LiesOver p.

Русский

Если p ∈ Spec(A) является примарным, существует примарный P в B с P LiesOver p.

LaTeX

$$∃ P, P.IsPrime ∧ P.LiesOver p$$

Lean4

instance self : FaithfullyFlat R R where
  submodule_ne_top m h
    r := Ideal.eq_top_iff_one _ |>.not.1 h.ne_top <| by simpa using show 1 ∈ (m • ⊤ : Ideal R) from r.symm ▸ ⟨⟩

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

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

Разделы

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

Аффилиация

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