ringConGen

Mathlib.RingTheory.Congruence.Defs

URI: https://scilib.ai/kg/mathlib#ringConGen

Lean4

/-- The inductively defined smallest ring congruence relation containing a given binary
relation. -/
def ringConGen [Add R] [Mul R] (r : R → R → Prop) : RingCon R
    where
  r := RingConGen.Rel r
  iseqv := ⟨RingConGen.Rel.refl, @RingConGen.Rel.symm _ _ _ _, @RingConGen.Rel.trans _ _ _ _⟩
  add' := RingConGen.Rel.add
  mul' := RingConGen.Rel.mul

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

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

Разделы

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

Аффилиация

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