ringConGen_of_ringCon — Mathlib

English

Congruence relations equal their generated smallest congruence.

Русский

Конгруэнтность равна самой минимально образующей её конгруэнтности.

LaTeX

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

Lean4

/-- Congruence relations equal the smallest congruence relation in which they are contained. -/
theorem ringConGen_of_ringCon (c : RingCon R) : ringConGen c = c :=
  le_antisymm (by rw [ringConGen_eq]; exact sInf_le fun _ _ => id) RingConGen.Rel.of

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