rel_iff — Mathlib

English

For a two-sided ideal I of a ring, the relation x ≡ y mod I holds iff x − y ∈ I.

Русский

Для двустороннего идеала I верно: x ≡ y mod I тогда и только тогда, когда x − y ∈ I.

LaTeX

$$I.ringCon x y ↔ x - y ∈ I$$

Lean4

theorem rel_iff (x y : R) : I.ringCon x y ↔ x - y ∈ I :=
  by
  rw [mem_iff]
  constructor
  · intro h; convert I.ringCon.sub h (I.ringCon.refl y); abel
  · intro h; convert I.ringCon.add h (I.ringCon.refl y) <;> abel

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