Theorems · Definition · commutative algebra

PowerBasis.equivOfMinpoly

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

pb.equivOfMinpoly pb' h is an equivalence of algebras with the same power basis, where "the same" means that they have identical minimal polynomials. See also PowerBasis.equivOfRoot which takes the hypothesis that each generator is a root of the other basis' minimal polynomial; PowerBasis.equivOfRoot is more general if A is not a field.

Defined in

Mathlib.RingTheory.PowerBasis

Cited by

8 results in Mathlib

Foundations

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

Assumes

RingCommRingAlgebraRingAlgebra