submodule_map_mul_reverse — Mathlib

English

The map reverse distributes over the product of submodules: (p * q).map reverse = q.map reverse * p.map reverse.

Русский

Обратное распределяется по произведению подмодулей: (p * q).map reverse = q.map reverse * p.map reverse.

LaTeX

$$$ (p * q).map (reverse) = q.map (reverse) * p.map (reverse) $$$

Lean4

/-- Like `Submodule.map_mul`, but with the multiplication reversed. -/
theorem submodule_map_mul_reverse (p q : Submodule R (CliffordAlgebra Q)) :
    (p * q).map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) =
      q.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) *
        p.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :=
  by simp_rw [reverse, Submodule.map_comp, Submodule.map_mul, Submodule.map_unop_mul]

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