Theorems · Definition · field theory

IntermediateField.extendScalars.orderIso

{K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → (F : IntermediateField K L) → { E // F ≤ E } ≃o IntermediateField (↥F) L

IntermediateField.extendScalars.orderIso bundles IntermediateField.extendScalars into an order isomorphism from { E : IntermediateField K L // F ≤ E } to IntermediateField F L. Its inverse is IntermediateField.restrictScalars.

Defined in: Mathlib.FieldTheory.IntermediateField.Basic
Cited by: 5 results in Mathlib
Foundations: Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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
IntermediateFieldstatement and proof · cited by 988
OrderIsostatement · cited by 874
IntermediateField.restrictScalarsproof · cited by 66
IntermediateField.extendScalarsproof · cited by 25

Cited by5

Results whose statement or proof uses this declaration.

IntermediateField.extendScalars_injectiveproof · cited by 0
IntermediateField.extendScalars.orderIso_applystatement and proof · cited by 0
IntermediateField.extendScalars.orderIso_symm_apply_coestatement and proof · cited by 0
IntermediateField.extendScalars_supproof · cited by 0
IntermediateField.extendScalars_infproof · cited by 0