Theorems · Theorem · field theory

Subfield.closure_induction

∀ {K : Type u} [inst : DivisionRing K] {s : Set K} {p : (x : K) → x ∈ Subfield.closure s → Prop},
  (∀ (x : K) (hx : x ∈ s), p x ⋯) →
    p 1 ⋯ →
      (∀ (x y : K) (hx : x ∈ Subfield.closure s) (hy : y ∈ Subfield.closure s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x : K) (hx : x ∈ Subfield.closure s), p x hx → p (-x) ⋯) →
          (∀ (x : K) (hx : x ∈ Subfield.closure s), p x hx → p x⁻¹ ⋯) →
            (∀ (x y : K) (hx : x ∈ Subfield.closure s) (hy : y ∈ Subfield.closure s), p x hx → p y hy → p (x * y) ⋯) →
              ∀ {x : K} (h : x ∈ Subfield.closure s), p x h

An induction principle for closure membership. If p holds for 1, and all elements of s, and is preserved under addition, negation, and multiplication, then p holds for all elements of the closure of s.

Defined in

Mathlib.Algebra.Field.Subfield.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionRing