Theorems · Theorem · ring theory

CliffordAlgebra.submodule_map_pow_reverse

∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (p : Submodule R (CliffordAlgebra Q)) (n : ℕ),
  Submodule.map CliffordAlgebra.reverse (p ^ n) = Submodule.map CliffordAlgebra.reverse p ^ n

Like Submodule.map_pow

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Cited by

2 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule