Theorems · Theorem · number theory

NumberField.InfinitePlace.exists_smul_eq_of_comap_eq

∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K]
  {w w' : NumberField.InfinitePlace K}, w.comap (algebraMap k K) = w'.comap (algebraMap k K) → ∃ σ, σ • w = w'

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsGalois