mod_mem_iff — Mathlib

English

In a Euclidean domain, for any ideal S and x, y with y ∈ S, we have x % y ∈ S iff x ∈ S.

Русский

В евклидовом кольце для любого идеала S и элементов x,y с y ∈ S выполнение x mod y ∈ S эквивалентно x ∈ S.

LaTeX

$$$x \\\\% y \\\\in S \\\\Leftrightarrow x \\\\in S$$$

Lean4

theorem mod_mem_iff {S : Ideal R} {x y : R} (hy : y ∈ S) : x % y ∈ S ↔ x ∈ S :=
  ⟨fun hxy => div_add_mod x y ▸ S.add_mem (S.mul_mem_right _ hy) hxy, fun hx =>
    (mod_eq_sub_mul_div x y).symm ▸ S.sub_mem hx (S.mul_mem_right _ hy)⟩
    -- see Note [lower instance priority]

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