English
Let I ⊆ A, J ⊆ B be submodules and N ⊆ M a submodule, with appropriate scalar-tower structure. Then (I • J) • N = I • (J • N).
Русский
Пусть I ⊆ A, J ⊆ B — подмодули, N ⊆ M — подмодуль, при условии существования нужной структуры скалярного тензора. Тогда (I • J) • N = I • (J • N).
LaTeX
$$$ (I \cdot J) \cdot N = I \cdot (J \cdot N) $$$
Lean4
protected theorem smul_assoc {B} [Semiring B] [Module R B] [Module A B] [Module B M] [IsScalarTower R A B]
[IsScalarTower R B M] [IsScalarTower A B M] (I : Submodule R A) (J : Submodule R B) (N : Submodule R M) :
(I • J) • N = I • J • N :=
le_antisymm
(smul_le.2 fun _ hrsij t htn ↦
smul_induction_on hrsij (fun r hr s hs ↦ smul_assoc r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn)) fun x y ↦
(add_smul x y t).symm ▸ add_mem)
(smul_le.2 fun r hr _ hsn ↦
smul_induction_on hsn (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn)
fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem)
