Theorems · Theorem · ring theory

StarAlgebra.adjoin_induction

∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {s : Set A}
  {p : (x : A) → x ∈ StarAlgebra.adjoin R s → Prop},
  (∀ (x : A) (h : x ∈ s), p x ⋯) →
    (∀ (r : R), p ((algebraMap R A) r) ⋯) →
      (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s),
            p x hx → p y hy → p (x * y) ⋯) →
          (∀ (x : A) (hx : x ∈ StarAlgebra.adjoin R s), p x hx → p (star x) ⋯) →
            ∀ {a : A} (ha : a ∈ StarAlgebra.adjoin R s), p a ha

If some predicate holds for all x ∈ (s : Set A) and this predicate is closed under the algebraMap, addition, multiplication and star operations, then it holds for a ∈ adjoin R s.

Defined in

Mathlib.Algebra.Star.Subalgebra

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingSemiringAlgebraStarRingStarModule