Theorems · Theorem · ring theory

TrivSqZeroExt.linearMap_ext

∀ {S : Type u_2} {R : Type u} {M : Type v} {N : Type u_3} [inst : Semiring S] [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module S R] [inst_5 : Module S M]
  [inst_6 : Module S N] ⦃f g : TrivSqZeroExt R M →ₗ[S] N⦄,
  (∀ (r : R), f (TrivSqZeroExt.inl r) = g (TrivSqZeroExt.inl r)) →
    (∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)) → f = g

This cannot be marked @[ext] as it ends up being used instead of LinearMap.prod_ext when working with R × M.

Defined in

Mathlib.Algebra.TrivSqZeroExt.Basic

Cited by

2 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModule