English
Let I and J be submodules of A and N a submodule of M in a compatible scalar-tower setting. Then the action distributes over the join: (I ⊔ J) • N = I • N ⊔ J • N.
Русский
Пусть I и J — подмодули A, N — подмодуль M в подходящей конфигурации скалярного тензора. Тогда действие распределяется по объединению: (I ⊔ J) • N = I • N ⊔ J • N.
LaTeX
$$$ (I \sqcup J) \cdot N = I \cdot N \sqcup J \cdot N $$$
Lean4
theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N :=
le_antisymm
(smul_le.mpr fun mn hmn p hp ↦ by
obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp)
(sup_le (smul_mono_left le_sup_left) <| smul_mono_left le_sup_right)
