nontrivial_tensorProduct_iff_left

English

If N is faithfully flat, then Nontrivial(M ⊗R N) iff Nontrivial M.

Русский

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

LaTeX

$$$\forall N\ [\text{Module }R N],\ [\mathrm{FaithfullyFlat}_R(N)] \Rightarrow \big( \mathrm{Nontrivial}(M \otimes_R N) \iff \mathrm{Nontrivial}(M) \big)$$$

Lean4

@[simp]
theorem nontrivial_tensorProduct_iff_left [Module.FaithfullyFlat R N] : Nontrivial (M ⊗[R] N) ↔ Nontrivial M := by
  simp [← not_iff_not, not_nontrivial_iff_subsingleton]

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