top_smul — Mathlib

English

For every submodule N, the top ideal acts as the identity: (⊤ : Ideal R) · N = N.

Русский

Для любого подподмодуля N тензорное действие единичного идеала даёт тот же самый подмодуль: (⊤ : Ideal R) · N = N.

LaTeX

$$$(\\top : Ideal R) \\cdot N = N$$$

Lean4

@[simp]
theorem top_smul : (⊤ : Ideal R) • N = N :=
  le_antisymm smul_le_right fun r hri => one_smul R r ▸ smul_mem_smul mem_top hri

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