Mathlib Map

Theorems · Theorem · number theory

NumberField.conj_basisMatrix

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.basisMatrix K).map ⇑(starRingEnd ℂ) =
    (Matrix.reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm NumberField.ComplexEmbedding.conjugate ⋯))
      (NumberField.basisMatrix K)
Defined in
Mathlib.NumberTheory.NumberField.EquivReindex
Cited by
1 results in Mathlib
Foundations
Depth 300 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldNumberField
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NumberField.sign_discr · cited by 1NumberField.sign_discrDFunLike.coe · cited by 62936DFunLike.coeRingHom · cited by 10189RingHomEquiv · cited by 8337EquivField · cited by 7404FieldComplex · cited by 5565ComplexAlgebra.algebraMap · cited by 4706Algebra.algebraMapMatrix · cited by 4303MatrixstarRingEnd · cited by 671starRingEndNumberField · cited by 653NumberFieldMatrix.ext · cited by 540Matrix.extNumberField.RingOfIntegers · cited by 413NumberField.RingOfIntegersEquiv.refl · cited by 274Equiv.reflMatrix.map · cited by 247Matrix.mapMatrix.reindex · cited by 102Matrix.reindexNumberField.ComplexEmbedding.conjugate · cited by 40ComplexEmbedding.conjugateNumberField.conj_basisMatrixCITED BYCITES

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.