mem_iff_eq_smul_generator — Mathlib

English

x ∈ S iff x is a scalar multiple of generator S.

Русский

x ∈ S эквивалентно тому, что x является скалярным произведением генератора S.

LaTeX

$$x ∈ S ↔ ∃ s ∈ R, x = s • generator S$$

Lean4

theorem mem_iff_eq_smul_generator (S : Submodule R M) [S.IsPrincipal] {x : M} : x ∈ S ↔ ∃ s : R, x = s • generator S :=
  by simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]

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