Theorems · Theorem · group theory

Submonoid.saturation_induction

∀ {M : Type u_1} [inst : MulOneClass M] {s : Submonoid M} {p : (x : M) → x ∈ s.saturation → Prop},
  (∀ (x : M) (hx : x ∈ s), p x ⋯) →
    (∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯) →
      (∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯) →
        ∀ {x : M} (hx : x ∈ s.saturation), p x hx

Defined in

Mathlib.Algebra.Group.Submonoid.Saturation

Cited by

1 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

MulOneClass