Mathlib Map

Theorems · Theorem · field theory

IsGalois.of_algEquiv

∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] {E' : Type u_4} [inst_2 : Field E']
  [inst_3 : Algebra F E'] [inst_4 : Algebra F E] [IsGalois F E] (f : E ≃ₐ[F] E'), IsGalois F E'
Defined in
Mathlib.FieldTheory.Galois.Basic
Cited by
3 results in Mathlib
Foundations
Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldFieldFieldAlgebraAlgebraIsGalois
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IntermediateField.LinearDisjoint.of_inf_eq_bot · cited by 2LinearDisjoint.of_inf_eq_…AlgEquiv.transfer_galois · cited by 2AlgEquiv.transfer_galoisIsGaloisGroup.normal_of_isGalois · cited by 0IsGaloisGroup.normal_of_i…Algebra · cited by 11388AlgebraField · cited by 7404FieldAlgEquiv · cited by 1681AlgEquivIsGalois · cited by 149IsGaloisIsGalois.of_algEquivCITED BYCITES

Cites4

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
  • AlgEquivstatement and proof · cited by 1,681
  • IsGaloisstatement and proof · cited by 149

Cited by3

Results whose statement or proof uses this declaration.