Some lemmas about linear functionals on division rings

This file proves some results on linear functionals on division semirings.

Main results

• LinearMap.surjective_iff_ne_zero: a linear functional f is surjective iff f ≠ 0.
• LinearMap.range_smulRight_apply: for a nonzero linear functional f and element x, the range of f.smulRight x is the span of the set {x}.

theorem LinearMap.surjective_iff_ne_zero {R : Type u_1} {M : Type u_2} [AddCommMonoid M] [DivisionSemiring R] [Module R M] {f : M →ₗ[R] R} : Function.Surjective ⇑f ↔ f ≠ 0

theorem LinearMap.surjective {R : Type u_1} {M : Type u_2} [AddCommMonoid M] [DivisionSemiring R] [Module R M] {f : M →ₗ[R] R} : f ≠ 0 → Function.Surjective ⇑f

Alias of the reverse direction of LinearMap.surjective_iff_ne_zero.

theorem LinearMap.range_smulRight_apply_of_surjective {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [AddCommMonoid M] [AddCommMonoid M₁] [Semiring R] [Module R M] [Module R M₁] {f : M →ₗ[R] R} (hf : Function.Surjective ⇑f) (x : M₁) : range (f.smulRight x) = Submodule.span R {x}

theorem LinearMap.range_smulRight_apply {R : Type u_1} {M : Type u_2} {M₁ : Type u_3} [AddCommMonoid M] [AddCommMonoid M₁] [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}