submodule_comap_pow_reverse — Mathlib

English

The comap under reverse commutes with exponentiation: (p^n).comap reverse = (p.comap reverse)^n.

Русский

Сопряжение через reverse сохраняет степени: (p^n).comap reverse = (p.comap reverse)^n.

LaTeX

$$$ (p^n).comap reverse = (p.comap reverse)^n $$$

Lean4

theorem submodule_comap_pow_reverse (p : Submodule R (CliffordAlgebra Q)) (n : ℕ) :
    (p ^ n).comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) =
      p.comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) ^ n :=
  by simp_rw [← submodule_map_reverse_eq_comap, submodule_map_pow_reverse]

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