equivOfRoot_symm — Mathlib

English

Let pb and pb' be power bases with h1 and h2 as above. Then the symmetric form of the root equivalence satisfies (pb.equivOfRoot pb' h1 h2).symm = pb'.equivOfRoot pb h2 h1.

Русский

Пусть pb и pb' —power-базисы с условиями h1, h2. Тогда симметричная форма эквивалентности корня удовлетворяет (pb.equivOfRoot pb' h1 h2).symm = pb'.equivOfRoot pb h2 h1.

LaTeX

$$$ (pb.equivOfRoot pb' h_1 h_2).symm = pb'.equivOfRoot pb h_2 h_1 $$$

Lean4

@[simp]
theorem equivOfRoot_symm (pb : PowerBasis A S) (pb' : PowerBasis A S') (h₁ : aeval pb.gen (minpoly A pb'.gen) = 0)
    (h₂ : aeval pb'.gen (minpoly A pb.gen) = 0) : (pb.equivOfRoot pb' h₁ h₂).symm = pb'.equivOfRoot pb h₂ h₁ :=
  rfl

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