Theorems · Definition · commutative algebra

PowerBasis.equivOfRoot

{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') →
                    (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0 →
                      (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0 → S ≃ₐ[A] S'

pb.equivOfRoot pb' h₁ h₂ is an equivalence of algebras with the same power basis, where "the same" means that pb is a root of pb's minimal polynomial and vice versa. See also PowerBasis.equivOfMinpoly which takes the hypothesis that the minimal polynomials are identical.

Defined in

Mathlib.RingTheory.PowerBasis

Cited by

6 results in Mathlib

Foundations

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

Assumes

RingCommRingAlgebraRingAlgebra