Theorems · Theorem · linear algebra

LinearMap.rTensor_surjective

∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} (Q : Type u_5) [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] {g : N →ₗ[R] P}, Function.Surjective ⇑g → Function.Surjective ⇑(LinearMap.rTensor Q g)

If g is surjective, then rTensor Q g is surjective

Defined in

Mathlib.LinearAlgebra.TensorProduct.RightExactness

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModule