mem_spanSingleton — Mathlib

English

An element x lies in spanSingleton S y if and only if x is a scalar multiple of y by some element of R.

Русский

Элемент x лежит в spanSingleton S y тогда и только тогда, когда x является скалярным кратным y на элементе из R.

LaTeX

$$$ x \in \operatorname{spanSingleton} S y \iff \exists z \in R, z \cdot y = x $$$

Lean4

@[simp]
theorem mem_spanSingleton {x y : P} : x ∈ spanSingleton S y ↔ ∃ z : R, z • y = x :=
  by
  rw [spanSingleton]
  exact Submodule.mem_span_singleton

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