instLE

Mathlib.RingTheory.Congruence.Basic

URI: https://scilib.ai/kg/mathlib#RingCon.instLE

Lean4

/-- For congruence relations `c, d` on a type `M` with multiplication and addition, `c ≤ d` iff
`∀ x y ∈ M`, `x` is related to `y` by `d` if `x` is related to `y` by `c`. -/
instance : LE (RingCon R) where le c d := ∀ ⦃x y⦄, c x y → d x y

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

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

Разделы

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

Аффилиация

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