Theorems · Theorem · linear algebra

TensorProduct.map_surjective

∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : Module R N] [inst_4 : Module R P] {g : N →ₗ[R] P},
  Function.Surjective ⇑g →
    ∀ {N' : Type u_6} {P' : Type u_7} [inst_5 : AddCommMonoid N'] [inst_6 : AddCommMonoid P'] [inst_7 : Module R N']
      [inst_8 : Module R P'] {g' : N' →ₗ[R] P'}, Function.Surjective ⇑g' → Function.Surjective ⇑(TensorProduct.map g g')

Defined in

Mathlib.LinearAlgebra.TensorProduct.RightExactness

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModuleAddCommMonoidAddCommMonoidModuleModule