Theorems · Definition · commutative algebra

Module.Presentation.tensor

{A : Type u} →
  [inst : CommRing A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module A M₁] →
              [inst_4 : Module A M₂] →
                Module.Presentation A M₁ → Module.Presentation A M₂ → Module.Presentation A (TensorProduct A M₁ M₂)

The presentation of the A-module M₁ ⊗[A] M₂ that is deduced from a presentation of M₁ and a presentation of M₂.

Defined in

Mathlib.Algebra.Module.Presentation.Tensor

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupModuleModule