Theorems · Theorem · number theory

NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (K →+* ℂ) → ℂ),
  (∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (NumberField.ComplexEmbedding.conjugate φ)) →
    ∀ (c : NumberField.mixedEmbedding.index K),
      ↑(((NumberField.mixedEmbedding.stdBasis K).repr ((NumberField.mixedEmbedding.commMap K) x)) c) =
        (NumberField.mixedEmbedding.matrixToStdBasis K).mulVec (x ∘ ⇑(NumberField.mixedEmbedding.indexEquiv K)) c

Let x : (K →+* ℂ) → ℂ such that x_φ = conj x_(conj φ) for all φ : K →+* ℂ, then the representation of commMap K x on stdBasis is given (up to reindexing) by the product of matrixToStdBasis by x.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Cited by

1 results in Mathlib

Foundations

Depth 299 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField