Theorems · Definition · field theory

IntermediateField.Lifts.carrier

{F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] → [inst_4 : Algebra F K] → IntermediateField.Lifts F E K → IntermediateField F E

The domain of a lift.

Defined in: Mathlib.FieldTheory.Extension
Cited by: 14 results in Mathlib
Foundations: Depth 46 from the axioms · uses propext, Quot.sound
Assumes: Field Field Field Algebra Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

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
IntermediateFieldstatement · cited by 988
IntermediateField.Liftsstatement and proof · cited by 18

Cited by17

Results whose statement or proof uses this declaration.

IntermediateField.Lifts.embstatement · cited by 11
IntermediateField.Lifts.unionproof · cited by 6
IntermediateField.exists_algHom_adjoin_of_splitsproof · cited by 4
IntermediateField.Lifts.le_iffstatement and proof · cited by 4
IntermediateField.Lifts.le_unionproof · cited by 3
IntermediateField.Lifts.IsExtendibleproof · cited by 2
IntermediateField.Lifts.carrier_unionstatement · cited by 1
IntermediateField.Lifts.eq_iff_le_carrier_eqstatement and proof · cited by 1
IntermediateField.Lifts.exists_lift_of_splitsstatement · cited by 1
IntermediateField.Lifts.exists_lift_of_splits'statement and proof · cited by 1
IntermediateField.Lifts.le_of_carrier_le_iSupstatement and proof · cited by 1
IntermediateField.Lifts.lt_iffstatement and proof · cited by 1