nontrivial_tensorProduct_iff_right

English

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

Русский

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

LaTeX

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

Lean4

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

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