Theorems · Definition · field theory

Polynomial.Gal.galActionHom

{F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] →
            [Fact (Polynomial.map (algebraMap F E) p).Splits] → p.Gal →* Equiv.Perm ↑(p.rootSet E)

Polynomial.Gal.galAction as a permutation representation

Defined in: Mathlib.FieldTheory.PolynomialGaloisGroup
Cited by: 6 results in Mathlib
Foundations: Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra Fact

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Set.Elemstatement and proof · cited by 7,166
Polynomialstatement and proof · cited by 5,681
Algebra.algebraMapstatement and proof · cited by 4,706
MonoidHomstatement · cited by 3,629
Factstatement and proof · cited by 2,726
Equiv.Permstatement · cited by 1,375
Polynomial.mapstatement and proof · cited by 806
Polynomial.Splitsstatement and proof · cited by 290
Polynomial.rootSetstatement and proof · cited by 101
Polynomial.Galstatement and proof · cited by 37

Cited by6

Results whose statement or proof uses this declaration.

Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_invstatement and proof · cited by 2
Polynomial.Gal.galActionHom_bijective_of_prime_degreestatement and proof · cited by 1
Polynomial.Gal.galActionHom_injectivestatement and proof · cited by 1
Polynomial.Gal.galActionHom_restrictstatement · cited by 1
Polynomial.Gal.galActionHom_bijective_of_prime_degree'statement and proof · cited by 0
Polynomial.Gal.galActionHom.congr_simpstatement and proof · cited by 0