mem_smul_top_iff — Mathlib

English

For a submodule N of M and an ideal I, and x ∈ N, x ∈ I • ⊤_N if and only if x ∈ I • N.

Русский

Для подподмодуля N ⊆ M и идеала I: x ∈ I • ⊤_N ⇔ x ∈ I • N, если x ∈ N.

LaTeX

$$$x \\in I \\cdot (\\top_N) \\iff x \\in I \\cdot N$$$

Lean4

theorem mem_smul_top_iff (N : Submodule R M) (x : N) : x ∈ I • (⊤ : Submodule R N) ↔ (x : M) ∈ I • N :=
  by
  have : Submodule.map N.subtype (I • ⊤) = I • N := by
    rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]
  simp [← this, -map_smul'']

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