equivOfMinpoly_gen — Mathlib

English

Let pb and pb' be power bases with h : minpoly A pb.gen = minpoly A pb'.gen. Then pb.equivOfMinpoly pb' h pb.gen = pb'.gen.

Русский

Пусть pb и pb' — power-базисы и minpoly pb.gen = minpoly pb'.gen. Тогда pb.equivOfMinpoly pb' h pb.gen = pb'.gen.

LaTeX

$$$ pb.equivOfMinpoly pb' h pb.gen = pb'.gen $$$

Lean4

@[simp]
theorem equivOfMinpoly_gen (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
    pb.equivOfMinpoly pb' h pb.gen = pb'.gen :=
  pb.equivOfRoot_gen pb' _ _

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