submodule_map_pow_reverse — Mathlib

English

The map reverse commutes with exponentiation of a submodule: (p^n).map reverse = (p.map reverse)^n.

Русский

Обратное коммутирует с возведением подмодуля в степень: (p^n).map reverse = (p.map reverse)^n.

LaTeX

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

Lean4

/-- Like `Submodule.map_pow` -/
theorem submodule_map_pow_reverse (p : Submodule R (CliffordAlgebra Q)) (n : ℕ) :
    (p ^ n).map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) =
      p.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) ^ n :=
  by simp_rw [reverse, Submodule.map_comp, Submodule.map_pow, Submodule.map_unop_pow]

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