mem_span_singleton_mul — Mathlib

English

For any y ∈ A, x ∈ span R {y} · P iff ∃ z ∈ P with y·z = x.

Русский

Для любого y ∈ A: x ∈ span{y} · P эквивалентно существованию z ∈ P такого что y·z = x.

LaTeX

$$$x \\in \\operatorname{span} R\\{y\\} \\cdot P \\quad\\iff\\quad \\exists z \\in P,\\; y \\cdot z = x$$$

Lean4

theorem mem_span_singleton_mul {x y : A} : x ∈ span R { y } * P ↔ ∃ z ∈ P, y * z = x := by
  simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map, mem_map, LinearMap.mul_apply_apply]

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