equivOfRoot_gen — Mathlib

English

Let pb and pb' be power bases as above with h1 and h2 as in the previous statement. Then pb.equivOfRoot pb' h1 h2 pb.gen = pb'.gen.

Русский

Пусть pb и pb' —power-базисы и имеются такие условия h1, h2, как выше. Тогда pb.equivOfRoot pb' h1 h2 pb.gen = pb'.gen.

LaTeX

$$$ pb.equivOfRoot pb' h_1 h_2 pb.gen = pb'.gen $$$

Lean4

@[simp]
theorem equivOfRoot_gen (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₂ pb.gen = pb'.gen :=
  pb.lift_gen _ h₂

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