Theorems · Theorem · number theory

NumberField.inverse_basisMatrix_mulVec_eq_repr

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)]
  (α : NumberField.RingOfIntegers K) (i : K →+* ℂ),
  (NumberField.basisMatrix K).transpose⁻¹.mulVec
      (fun j => (NumberField.canonicalEmbedding K) ((algebraMap (NumberField.RingOfIntegers K) K) α) j) 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 304 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberFieldDecidableEq