rTensor_reflects_triviality — Mathlib

English

If N ⊗_R M is a singleton, then N is a singleton, under FaithfullyFlat assumptions.

Русский

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

LaTeX

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

Lean4

theorem rTensor_reflects_triviality [FaithfullyFlat R M] (N : Type*) [AddCommGroup N] [Module R N]
    [h : Subsingleton (N ⊗[R] M)] : Subsingleton N := by
  revert h; change _ → _; contrapose!
  intro h
  infer_instance

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