tensor — Mathlib

English

The tensor product of free modules is free: if M and N are free, then M ⊗_R N is free over S.

Русский

Тензорное произведение свободных модулей освобождает: если M и N свободны, то M ⊗_R N свободен над S.

LaTeX

$$Module.Free S (TensorProduct R M N)$$

Lean4

instance tensor : Module.Free S (M ⊗[R] N) :=
  let ⟨bM⟩ := exists_basis (R := S) (M := M)
  let ⟨bN⟩ := exists_basis (R := R) (M := N)
  of_basis (bM.2.tensorProduct bN.2)

Похожие утверждения