instFintypeElemCarrierOfNormalOfDecidableEqOfAlgEquiv

English

For a normal extension with the given hypotheses, the carrier.Elem of c.carrier is finite (has a finite type).

Русский

Для нормального расширения при данных предпосылках множество элементов носителя c.carrier является конечным (имеет конечный тип).

LaTeX

$$$\\operatorname{Fintype}(c.carrier.Elem)$$$

Lean4

instance [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] (c : ConjRootClass K L) : Fintype c.carrier :=
  Quotient.recOnSubsingleton c fun x =>
    .ofFinset ((Finset.univ (α := L ≃ₐ[K] L)).image (· x))
      (fun _ ↦ by simp [← isConjRoot_iff_exists_algEquiv, ← mk_eq_mk])

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