English
If two linear maps f,g: tsze_R M → N agree on inl(r) for all r and on inr(m) for all m, then f = g. This is the product-extensionality principle for linear maps on tsze_R M.
Русский
Если две линейные карты совпадают на частях inl(r) и inr(m), то они совпадают везде: f = g.
LaTeX
$$$\big( \forall r, f(\mathrm{inl}(r)) = g(\mathrm{inl}(r)) \big) \land \big( \forall m, f(\mathrm{inr}(m)) = g(\mathrm{inr}(m)) \big) \Rightarrow f = g$$$
Lean4
/-- This cannot be marked `@[ext]` as it ends up being used instead of `LinearMap.prod_ext` when
working with `R × M`. -/
theorem linearMap_ext {N} [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [AddCommMonoid N] [Module S R] [Module S M]
[Module S N] ⦃f g : tsze R M →ₗ[S] N⦄ (hl : ∀ r, f (inl r) = g (inl r)) (hr : ∀ m, f (inr m) = g (inr m)) : f = g :=
LinearMap.prod_ext (LinearMap.ext hl) (LinearMap.ext hr)
