instIsEquiv — Mathlib

English

The relation of being a conjugate root over a base field forms an equivalence relation on the target field extension.

Русский

Отношение «быть сопряжённым корнем над базовым полем» образует эквивелентность на расширении.

LaTeX

$$$\text{IsEquiv } L (IsConjRoot K)$$$

Lean4

instance : IsEquiv L (IsConjRoot K) :=
  letI := IsConjRoot.setoid K L
  inferInstanceAs <| IsEquiv L (· ≈ ·)

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