Theorems · Definition · commutative algebra

IsGaloisGroup.mulEquivAlgEquiv

(G : Type u_1) →
  [inst : Group G] →
    (A : Type u_2) →
      (B : Type u_3) →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [IsDomain B] →
              [inst_4 : Algebra A B] →
                [FaithfulSMul A B] →
                  [inst_6 : MulSemiringAction G B] → [IsGaloisGroup G A B] → [Finite G] → G ≃* B ≃ₐ[A] B

If G is a finite Galois group for B/A, then G is isomorphic to Gal(B/A).

Defined in

Mathlib.RingTheory.IsGaloisGroup.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

GroupCommRingCommRingIsDomainAlgebraFaithfulSMulMulSemiringActionIsGaloisGroupFinite