Theorems · Definition · number theory
NumberField.mixedEmbedding.matrixToStdBasis
(K : Type u_1) → [inst : Field K] → Matrix (NumberField.mixedEmbedding.index K) (NumberField.mixedEmbedding.index K) ℂ
The matrix that gives the representation on stdBasis of the image by commMap of an
element x of (K →+* ℂ) → ℂ fixed by the map x_φ ↦ conj x_(conjugate φ),
see stdBasis_repr_eq_matrixToStdBasis_mul.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fieldstatement and proof · cited by 7,404
- Complexstatement · cited by 5,565
- Matrixstatement · cited by 4,303
- Complex.Iproof · cited by 866
- Matrix.vecConsproof · cited by 852
- Matrix.vecEmptyproof · cited by 832
- NumberField.InfinitePlaceproof · cited by 604
- Matrix.ofproof · cited by 336
- Matrix.diagonalproof · cited by 314
- NumberField.InfinitePlace.IsRealproof · cited by 301
- NumberField.InfinitePlace.IsComplexproof · cited by 272
Cited by3
Results whose statement or proof uses this declaration.
- NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasisproof · cited by 4
- NumberField.mixedEmbedding.det_matrixToStdBasisstatement · cited by 1
- NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mulstatement · cited by 1