Pointwise equality on generated submodules #
This file provides a small extension principle for semilinear maps that agree on a submodule and on one additional generator.
theorem
LinearMap.eqOn_sup_span_singleton
{R : Type u₁}
{R₂ : Type u₂}
{M : Type u₃}
{M₂ : Type u₄}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{σ : R →+* R₂}
(f : M →ₛₗ[σ] M₂)
{g : M →ₛₗ[σ] M₂}
{W : Submodule R M}
{x : M}
(hW : Set.EqOn ⇑f ⇑g ↑W)
(hx : f x = g x)
:
Two semilinear maps that agree on W and at x agree on W ⊔ R ∙ x.