Theorems · Theorem · commutative algebra

PowerBasis.equivOfMinpoly_map

∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] {S' : Type u_7} [inst_2 : CommRing S']
  [inst_3 : Algebra A S] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S')
  (h : minpoly A pb.gen = minpoly A (pb.map e).gen), pb.equivOfMinpoly (pb.map e) h = e

Defined in

Mathlib.RingTheory.PowerBasis

Cited by

0 results in Mathlib

Foundations

Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingCommRingCommRingAlgebraAlgebra