equivOfMinpoly_symm — Mathlib

English

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

Русский

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

LaTeX

$$$ (pb.equivOfMinpoly pb' h).symm = pb'.equivOfMinpoly pb h.symm $$$

Lean4

@[simp]
theorem equivOfMinpoly_symm (pb : PowerBasis A S) (pb' : PowerBasis A S') (h : minpoly A pb.gen = minpoly A pb'.gen) :
    (pb.equivOfMinpoly pb' h).symm = pb'.equivOfMinpoly pb h.symm :=
  rfl

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