instDecidableEqOfNormalOfFintypeAlgEquiv

English

Induction principle for ConjRootClass: to prove a property for any c, it suffices to prove it for all mk K x with x ∈ L.

Русский

Индуктивный принцип для ConjRootClass: достаточен переход по всем mk K x.

LaTeX

$$Ind {motive : ConjRootClass K L → Prop} (h : ∀ x : L, motive (mk K x)) (c : ConjRootClass K L) : motive c$$

Lean4

instance [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] : DecidableEq (ConjRootClass K L) :=
  Quotient.decidableEq (d := IsConjRoot.decidable)

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