mul_eq_map₂ — Mathlib

English

For submodules M,N of A over R, their product equals the image of the bilinear multiplication map via map₂.

Русский

Для подмодулей M и N подмодуля A над R их произведение равно образу билинейного отображения умножения через map₂.

LaTeX

$$$M \\cdot N = \\mathrm{map}_2\\bigl( \\mathrm{LinearMap.mul}_R A \\bigr) M N$$$

Lean4

theorem mul_eq_map₂ : M * N = map₂ (LinearMap.mul R A) M N :=
  le_antisymm (mul_le.mpr fun _m hm _n ↦ apply_mem_map₂ _ hm) (map₂_le.mpr fun _m hm _n ↦ mul_mem_mul hm)

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