ne_conjugate — Mathlib

English

If w2 is ramified, then w1.embedding is not conjugate to the complex conjugate of w2.embedding.

Русский

Если w2 разомкнут, то w1.embedding не конъюгирован к сопряжённому w2.embedding.

LaTeX

$$$w_2\\text{ isRamified }\\Rightarrow w_1.\\text{embedding} \\neq \\text{ComplexEmbedding}.conjugate(w_2. embedding)$$$

Lean4

theorem ne_conjugate {w₁ w₂ : InfinitePlace K} (h : w₂.IsRamified k) :
    w₁.embedding ≠ ComplexEmbedding.conjugate w₂.embedding :=
  by
  by_cases h_eq : w₁ = w₂
  · rw [isRamified_iff, isComplex_iff] at h
    exact Ne.symm (h_eq ▸ h.1)
  · contrapose! h_eq
    rw [← mk_embedding w₁, h_eq, mk_conjugate_eq, mk_embedding]

Похожие утверждения