lTensor — Mathlib

English

If M' is IsSmulRegular with respect to r, then the left tensor product M ⊗_R M' is IsSmulRegular with respect to r.

Русский

Если M' удовлетворяет IsSmulRegular по r, то левый тензорный произведение M ⊗_R M' также регулярна по r.

LaTeX

$$$IsSmulRegular\; (M\otimes_R M')\; r$ given IsSmulRegular on M'.$$

Lean4

theorem lTensor : IsSMulRegular (M ⊗[R] M') r :=
  have h1 := congrArg DFunLike.coe (LinearMap.lTensor_smul_action M M' r)
  h1.subst (Module.Flat.lTensor_preserves_injective_linearMap _ h)

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