mem_iff_generator_dvd — Mathlib

English

If N ≤ O and ϕ: O → R, with (ϕ.submoduleImage N).IsPrincipal, then generator(ϕ.submoduleImage N) divides ϕ⟨x,hNO hx⟩ for x ∈ N.

Русский

Если N ≤ O и ϕ: O → R, и (ϕ.submoduleImage N).IsPrincipal, тогда генератор(ϕ.submoduleImage N) делит ϕ(⟨x,hNO hx⟩).

LaTeX

$$generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, hNO hx⟩$$

Lean4

theorem mem_iff_generator_dvd (S : Ideal R) [S.IsPrincipal] {x : R} : x ∈ S ↔ generator S ∣ x :=
  (mem_iff_eq_smul_generator S).trans (exists_congr fun a => by simp only [mul_comm, smul_eq_mul])

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