rTensor

Mathlib.RingTheory.Regular.IsSMulRegular

URI: https://scilib.ai/kg/mathlib#IsSMulRegular.rTensor

← MathLib Explorer

English

If M' is IsSmulRegular with respect to r, then M' ⊗_R M is IsSmulRegular with respect to r.

Русский

Если M' регулярна по r, то M' ⊗_R M регулярна по r.

LaTeX

$$$IsSmulRegular\; (M'\otimes_R M)\; r$ from IsSmulRegular of M'.$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru