lTensor_reflects_triviality — Mathlib

English

If M is faithfully flat and N ⊗_R M is trivial, then N is trivial.

Русский

Если M плоско и N ⊗_R M тривиален, то N тривиален.

LaTeX

$$Subsingleton (N ⊗_R M) ⇒ Subsingleton N$$

Lean4

theorem lTensor_reflects_triviality [FaithfullyFlat R M] (N : Type*) [AddCommGroup N] [Module R N]
    [Subsingleton (M ⊗[R] N)] : Subsingleton N :=
  by
  haveI : Subsingleton (N ⊗[R] M) := (TensorProduct.comm R N M).toEquiv.injective.subsingleton
  apply rTensor_reflects_triviality R M

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