Theorems · Theorem · linear algebra
CliffordAlgebraComplex.toComplex_involute
∀ (c : CliffordAlgebra CliffordAlgebraComplex.Q), CliffordAlgebraComplex.toComplex (CliffordAlgebra.involute c) = (starRingEnd ℂ) (CliffordAlgebraComplex.toComplex c)
CliffordAlgebra.involute is analogous to Complex.conj.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement and proof · cited by 25,697
- RingHomstatement · cited by 10,189
- Complexstatement and proof · cited by 5,565
- AlgHomstatement · cited by 3,236
- one_smulproof · cited by 1,374
- Complex.Iproof · cited by 866
- starRingEndstatement and proof · cited by 671
- AlgHom.compproof · cited by 501
- map_negproof · cited by 378
- CliffordAlgebrastatement and proof · cited by 309
- AlgEquiv.toAlgHomproof · cited by 273
Cited by1
Results whose statement or proof uses this declaration.
- CliffordAlgebraComplex.ofComplex_conjproof · cited by 0