Theorems · Theorem · field theory

IntermediateField.adjoin_induction

∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {s : Set E}
  {p : (x : E) → x ∈ IntermediateField.adjoin F s → Prop},
  (∀ (x : E) (hx : x ∈ s), p x ⋯) →
    (∀ (x : F), p ((algebraMap F E) x) ⋯) →
      (∀ (x y : E) (hx : x ∈ IntermediateField.adjoin F s) (hy : y ∈ IntermediateField.adjoin F s),
          p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x : E) (hx : x ∈ IntermediateField.adjoin F s), p x hx → p x⁻¹ ⋯) →
          (∀ (x y : E) (hx : x ∈ IntermediateField.adjoin F s) (hy : y ∈ IntermediateField.adjoin F s),
              p x hx → p y hy → p (x * y) ⋯) →
            ∀ {x : E} (h : x ∈ IntermediateField.adjoin F s), p x h

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

Cited by

2 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebra