mul_mem_smul_iff — Mathlib

English

If x is a non-zero-divisor in S, then x·y ∈ x·p iff y ∈ p.

Русский

Если x не нулевой делитель, тогда x·y ∈ x·p эквивалентно y ∈ p.

LaTeX

$$$x \\in \\mathrm{nonZeroDivisors}(S) \\Rightarrow x \\cdot y \\in x \\cdot p \\;\\Leftrightarrow\\; y \\in p$$$

Lean4

theorem mul_mem_smul_iff {S} [CommRing S] [Algebra R S] {x : S} {p : Submodule R S} {y : S}
    (hx : x ∈ nonZeroDivisors S) : x * y ∈ x • p ↔ y ∈ p := by
  simp [mem_smul_pointwise_iff_exists, mul_cancel_left_mem_nonZeroDivisors hx]

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