Theorems · Theorem · field theory
IsGalois.of_equiv_equiv
∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {M : Type u_5} {N : Type u_6}
[inst_3 : Field N] [inst_4 : Field M] [inst_5 : Algebra M N] [h : IsGalois F E] {f : F ≃+* M} {g : E ≃+* N},
(algebraMap M N).comp ↑f = (↑g).comp (algebraMap F E) → IsGalois M N- Defined in
- Mathlib.FieldTheory.Galois.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- RingHomstatement · cited by 10,189
- Fieldstatement and proof · cited by 7,404
- Algebra.algebraMapstatement and proof · cited by 4,706
- RingEquivstatement and proof · cited by 1,147
- RingHom.compstatement and proof · cited by 899
- RingHomClass.toRingHomstatement and proof · cited by 746
- IsGaloisstatement and proof · cited by 149
- Algebra.IsSeparable.of_equiv_equivproof · cited by 6
- isGalois_iffproof · cited by 2
- Normal.of_equiv_equivproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_powproof · cited by 1