span_singleton_smul_le — Mathlib

English

If r is a unit in R, then R ∙ (r • x) = R ∙ x.

Русский

Если r является единицей в R, то R ∙ (r • x) = R ∙ x.

LaTeX

$$$$ \\text{If } r \\text{ is a unit } R \\cdot (r \\cdot x) = R \\cdot x. $$$$

Lean4

theorem span_singleton_smul_le {S} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : M) : (R ∙ r • x) ≤ R ∙ x :=
  by
  rw [span_le, Set.singleton_subset_iff, SetLike.mem_coe]
  exact smul_of_tower_mem _ _ (mem_span_singleton_self _)

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