one_smul — Mathlib

English

The unit submodule acts trivially: 1 • N = N.

Русский

Единичный подмодуль действует тривиально: 1 • N = N.

LaTeX

$$$ (1 : \text{Submodule } R A) \cdot N = N $$$

Lean4

protected theorem one_smul : (1 : Submodule R A) • N = N :=
  by
  refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
  · obtain ⟨r, rfl⟩ := hr
    rw [LinearMap.toSpanSingleton_apply, smul_one_smul]; exact N.smul_mem r hm
  · rw [← one_smul A m]; exact smul_mem_smul (one_le.mp le_rfl) hm

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