coe_stabilizer_mk — Mathlib

English

The cardinality of the stabilizer is 1 or 2, depending on ramification.

Русский

Кардинал стабилизатора равен 1 или 2 в зависимости от размежевания.

LaTeX

$$$|Stab w| = 1 \\lor |Stab w| = 2$$$

Lean4

theorem _root_.NumberField.ComplexEmbedding.IsConj.coe_stabilizer_mk {φ : K →+* ℂ} (h : ComplexEmbedding.IsConj φ σ) :
    (Stab (mk φ) : Set (K ≃ₐ[k] K)) = { 1, σ } := by
  ext
  rw [SetLike.mem_coe, mem_stabilizer_mk_iff, Set.mem_insert_iff, Set.mem_singleton_iff, ← h.ext_iff, eq_comm (a := σ)]

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