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