lTensor_nontrivial

Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

URI: https://scilib.ai/kg/mathlib#Module.FaithfullyFlat.lTensor_nontrivial

← MathLib Explorer

English

If M is faithfully flat over R, then N ⊗_R M is nontrivial for nontrivial N.

Русский

Если M над R плоско и верно, то N ⊗ M не тривиален для не тривиального N.

LaTeX

$$Nontrivial (N ⊗_R M) for Nontrivial N$$

Lean4

instance lTensor_nontrivial [FaithfullyFlat R M] (N : Type*) [AddCommGroup N] [Module R N] [Nontrivial N] :
    Nontrivial (M ⊗[R] N) :=
  TensorProduct.comm R M N |>.toEquiv.nontrivial

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

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

Разделы

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

Аффилиация

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