Theorems · Definition · ring theory
CliffordAlgebra.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} → CliffordAlgebra Q →ₗ[R] CliffordAlgebra QGrade reversion, inverting the multiplication order of basis vectors. Also called transpose in some literature.
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- LinearMapstatement · cited by 10,215
- LinearMap.compproof · cited by 1,642
- LinearEquiv.symmproof · cited by 1,461
- LinearEquiv.toLinearMapproof · cited by 1,171
- QuadraticFormstatement and proof · cited by 507
- CliffordAlgebrastatement · cited by 309
- AlgHom.toLinearMapproof · cited by 254
- MulOpposite.opLinearEquivproof · cited by 44
Cited by53
Results whose statement or proof uses this declaration.
- CliffordAlgebra.reverse_ιstatement · cited by 12
- CliffordAlgebra.reverse.commutesstatement and proof · cited by 10
- CliffordAlgebra.contractRightproof · cited by 9
- CliffordAlgebra.left_inductionproof · cited by 8
- CliffordAlgebra.reverse.map_mulstatement and proof · cited by 8
- CliffordAlgebra.foldlproof · cited by 8
- CliffordAlgebra.contractRight_eqstatement · cited by 5
- CliffordAlgebra.foldr_reversestatement · cited by 5
- CliffordAlgebra.reverse_reversestatement · cited by 4
- CliffordAlgebra.reverseEquivproof · cited by 3
- CliffordAlgebra.reverse_involutivestatement · cited by 3
- CliffordAlgebra.star_defstatement · cited by 3