range_smulRight_apply — Mathlib

English

If f ≠ 0 and f: M →ₗ[R] R, then for any x ∈ M₁ the range of f.smulRight x equals span_R{ x }.

Русский

Если f ≠ 0 и f: M →ₗ[R] R, то для любого x ∈ M₁ образ f.smulRight x равен span_R{ x }.

LaTeX

$$$ \mathrm{range}(f \smulRight x) = \operatorname{span}_R \{ x \}$$$

Lean4

theorem range_smulRight_apply [DivisionSemiring R] [Module R M] [Module R M₁] {f : M →ₗ[R] R} (hf : f ≠ 0) (x : M₁) :
    range (f.smulRight x) = Submodule.span R { x } :=
  range_smulRight_apply_of_surjective (f.surjective hf) x

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