Theorems · Theorem · number theory

NumberField.canonicalEmbedding_eq_basisMatrix_mulVec

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K),
  (NumberField.canonicalEmbedding K) α =
    (NumberField.basisMatrix K).transpose.mulVec fun i =>
      ↑((((NumberField.integralBasis K).reindex (NumberField.equivReindex K).symm).repr α) i)

Defined in: Mathlib.NumberTheory.NumberField.EquivReindex
Cited by: 1 results in Mathlib
Foundations: Depth 302 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field NumberField

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites30

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
RingHom.idstatement · cited by 18,349
RingHomstatement and proof · cited by 10,189
Fieldstatement and proof · cited by 7,404
Complexstatement and proof · cited by 5,565
Finsuppstatement · cited by 5,255
Finset.sumproof · cited by 5,195
Equiv.symmstatement and proof · cited by 3,681
Finset.univproof · cited by 3,473
LinearEquivstatement · cited by 3,317
Finset.sum_congrproof · cited by 2,323
mul_commproof · cited by 2,262

Cited by1

Results whose statement or proof uses this declaration.

NumberField.inverse_basisMatrix_mulVec_eq_reprproof · cited by 1