iff_rTensor_injectiveₛ — Mathlib

English

A retract of a flat module is flat.

Русский

Возвращаемый модуль от плоского модуля также плоский.

LaTeX

$$$\text{of_retract }(i,r,h):\; \text{Flat } R N$$$

Lean4

/-- An easier-to-use version of `Module.flat_iff`, with finiteness conditions removed. -/
theorem iff_rTensor_injectiveₛ :
    Flat R M ↔
      ∀ ⦃P : Type u⦄ [AddCommMonoid P] [Module R P] (N : Submodule R P), Function.Injective (N.subtype.rTensor M) :=
  ⟨fun _ _ _ _ _ ↦ rTensor_preserves_injective_linearMap _ Subtype.val_injective, fun h ↦ ⟨fun _ _ _ _ _ _ ↦ h _⟩⟩

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