linearOrderOverring

Mathlib.RingTheory.Valuation.ValuationSubring

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

← MathLib Explorer

English

The set { S | A ≤ S } can be given a linear order compatible with inclusion.

Русский

Множество { S | A ≤ S } можно снабдить линейным порядком, совместимым с включением.

LaTeX

$$LinearOrder { S // A ≤ S }$$

Lean4

instance linearOrderOverring : LinearOrder { S // A ≤ S }
    where
  le_total := (le_total_ideal A).1
  max_def a b := congr_fun₂ sup_eq_maxDefault a b
  toDecidableLE := _

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

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

Разделы

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

Аффилиация

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