coeSubmodule_le_coeSubmodule — Mathlib

English

The image of the bottom ideal is the bottom submodule: coeSubmodule_bot.

Русский

Образ нулевого идеала — нулевой подмодуль.

LaTeX

$$coeSubmodule_bot : coeSubmodule S (⊥ : Ideal} R) = ⊥$$

Lean4

@[mono]
theorem coeSubmodule_le_coeSubmodule (h : M ≤ nonZeroDivisors R) {I J : Ideal R} :
    coeSubmodule S I ≤ coeSubmodule S J ↔ I ≤ J :=
  -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify the value of `f` here:

  Submodule.map_le_map_iff_of_injective (f := Algebra.linearMap R S) (IsLocalization.injective _ h) _ _

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