ringConGen_idem — Mathlib

English

ringConGen is idempotent: ringConGen(ringConGen r) = ringConGen r.

Русский

ringConGen(idempotent) ≡ ringConGen(r) = ringConGen(r).

LaTeX

$$$$ \operatorname{ringConGen}(\operatorname{ringConGen}(r)) = \operatorname{ringConGen}(r) $$$$

Lean4

/-- The map sending a binary relation to the smallest congruence relation in which it is
contained is idempotent. -/
theorem ringConGen_idem (r : R → R → Prop) : ringConGen (ringConGen r) = ringConGen r :=
  ringConGen_of_ringCon _

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