submodule_comap_mul_reverse — Mathlib

English

The comap under reverse distributes over multiplication: (p * q).comap reverse = q.comap reverse * p.comap reverse.

Русский

Сопряжение через reverse распределяется по умножению: (p * q).comap reverse = q.comap reverse * p.comap reverse.

LaTeX

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

Lean4

theorem submodule_comap_mul_reverse (p q : Submodule R (CliffordAlgebra Q)) :
    (p * q).comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) =
      q.comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) *
        p.comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :=
  by simp_rw [← submodule_map_reverse_eq_comap, submodule_map_mul_reverse]

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