ofPrime_le_of_le

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.ofPrime_le_of_le

← MathLib Explorer

English

Equality of idealOfLE with respect to a prime coarsening equals the prime ideal.

Русский

Равенство idealOfLE по прайм-упрощению равно простому идеалу.

LaTeX

$$idealOfLE A (ofPrime A P) (le_ofPrime A P) = P$$

Lean4

theorem ofPrime_le_of_le (P Q : Ideal A) [P.IsPrime] [Q.IsPrime] (h : P ≤ Q) : ofPrime A Q ≤ ofPrime A P :=
  fun _x ⟨a, s, hs, he⟩ => ⟨a, s, fun c => hs (h c), he⟩

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

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

Разделы

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

Аффилиация

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