English
Two linear maps from Unitization R A to N that agree on all inl r and on all inr a are equal.
Русский
Два линейных отображения от Unitization R A в N совпадают на всех inl r и на всех inr a, значит они равны.
LaTeX
$$$[Semiring S] [AddCommMonoid R] [AddCommMonoid A] [AddCommMonoid N] [Module S R] [Module S A] [Module S N] ⟂ f g : Unitization R A →_{[S]} N, \\\\forall r, f(inl r) = g(inl r) \\\\forall a, f(inr a) = g(inr a) \\\\Rightarrow f = g.$$$
Lean4
/-- This cannot be marked `@[ext]` as it ends up being used instead of `LinearMap.prod_ext` when
working with `R × A`. -/
theorem linearMap_ext {N} [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [AddCommMonoid N] [Module S R] [Module S A]
[Module S N] ⦃f g : Unitization R A →ₗ[S] N⦄ (hl : ∀ r, f (inl r) = g (inl r)) (hr : ∀ a : A, f a = g a) : f = g :=
LinearMap.prod_ext (LinearMap.ext hl) (LinearMap.ext hr)
