smul_eq_map₂ — Mathlib

English

The I • N construction is equal to the map₂ construction with the bilinear map (i, n) ↦ i • n.

Русский

Конструкция I • N равна конструкции map₂ с билинейным отображением (i, n) ↦ i • n.

LaTeX

$$$I \\cdot N = \\operatorname{Submodule.map_2}(\\operatorname{LinearMap.lsmul}\\ R\\ M)\\ I\\ N$$$

Lean4

theorem smul_eq_map₂ : I • N = Submodule.map₂ (LinearMap.lsmul R M) I N :=
  le_antisymm (smul_le.mpr fun _m hm _n ↦ Submodule.apply_mem_map₂ _ hm) (map₂_le.mpr fun _m hm _n ↦ smul_mem_smul hm)

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