Theorems · Theorem · linear algebra

TensorProduct.AlgebraTensorModule.ker_mapOfCompatibleSMul

∀ {R : Type u_1} (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (M : Type u_4)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] {N : Type u_5}
  [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : Module A N] [inst_10 : IsScalarTower R A N],
  (TensorProduct.mapOfCompatibleSMul A R A M N).ker =
    Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}

Defined in

Mathlib.LinearAlgebra.TensorProduct.Quotient

Cited by

0 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAddCommGroupModuleModuleIsScalarTowerAddCommGroupModuleModuleIsScalarTower