nat_card_stabilizer_eq_one_or_two

English

The natural-card of the stabilizer is either 1 or 2.

Русский

Натуральная карта стабилизатора равна 1 или 2.

LaTeX

$$$\\operatorname{Nat}.card(\\operatorname{Stab} w) = 1 \\lor \\operatorname{Nat}.card(\\operatorname{Stab} w) = 2$$$

Lean4

theorem nat_card_stabilizer_eq_one_or_two : Nat.card (Stab w) = 1 ∨ Nat.card (Stab w) = 2 := by
  classical
  rw [← SetLike.coe_sort_coe, ← mk_embedding w]
  by_cases h : ∃ σ, ComplexEmbedding.IsConj (k := k) (embedding w) σ
  · obtain ⟨σ, hσ⟩ := h
    simp only [hσ.coe_stabilizer_mk, Nat.card_eq_fintype_card, card_ofFinset, Set.toFinset_singleton]
    by_cases 1 = σ
    · left; simp [*]
    · right; simp [*]
  · push_neg at h
    left
    trans Nat.card ({ 1 } : Set (K ≃ₐ[k] K))
    · congr with x
      simp only [SetLike.mem_coe, mem_stabilizer_mk_iff, Set.mem_singleton_iff, or_iff_left_iff_imp, h x,
        IsEmpty.forall_iff]
    · simp

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