English
For M,N ⊆ A, the comap along the opposite equivalence distributes over multiplication: comap (op.symm) (M * N) = comap (op.symm) N * comap (op.symm) M.
Русский
Для подмодулов M,N ⊆ A выполняется распределение по отображению обратно: comap (op.symm) (M * N) = comap (op.symm) N * comap (op.symm) M.
LaTeX
$$$\\mathrm{comap}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) (M \\cdot N) = \\mathrm{comap}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) N \\cdot \\mathrm{comap}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) M$$$
Lean4
theorem comap_unop_mul :
comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) N *
comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M :=
by simp_rw [← map_equiv_eq_comap_symm, map_op_mul]
