iff_lTensor_injectiveₛ — Mathlib

English

Module.Flat R M is equivalent to the property that for all P, (N.subtype.rTensor M) is injective.

Русский

Module.Flat R M эквивалентно тому, что для всех P отображение N.subtype.rTensor M инъективно.

LaTeX

$$Module.Flat R M ↔ ∀ ⦃P⦄ [AddCommMonoid P] [Module R P] (N : Submodule R P), Injective (N.subtype.rTensor M)$$

Lean4

theorem iff_lTensor_injectiveₛ :
    Flat R M ↔
      ∀ ⦃P : Type u⦄ [AddCommMonoid P] [Module R P] (N : Submodule R P), Function.Injective (N.subtype.lTensor M) :=
  by simp_rw [iff_rTensor_injectiveₛ, LinearMap.lTensor_inj_iff_rTensor_inj]

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