Theorems · Theorem · ring theory

StarAlgebra.adjoin_induction_subtype

∀ {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 : ↥(StarAlgebra.adjoin R s) → Prop} (a : ↥(StarAlgebra.adjoin R s)),
  (∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩) →
    (∀ (r : R), p ((algebraMap R ↥(StarAlgebra.adjoin R s)) r)) →
      (∀ (x y : ↥(StarAlgebra.adjoin R s)), p x → p y → p (x + y)) →
        (∀ (x y : ↥(StarAlgebra.adjoin R s)), p x → p y → p (x * y)) →
          (∀ (x : ↥(StarAlgebra.adjoin R s)), p x → p (star x)) → p a

The difference with StarSubalgebra.adjoin_induction is that this acts on the subtype.

Defined in

Mathlib.Algebra.Star.Subalgebra

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingSemiringAlgebraStarRingStarModule