Theorems · Theorem · ring theory

SkewMonoidAlgebra.induction

∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] {p : SkewMonoidAlgebra M α → Prop} (f : SkewMonoidAlgebra M α),
  p 0 →
    (∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α),
        a ∉ f.support → b ≠ 0 → p f → p (SkewMonoidAlgebra.single a b + f)) →
      p f

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Single

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoid