Theorems · Theorem · ring theory

AddMonoidAlgebra.induction_linear

∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {motive : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M),
  motive 0 →
    (∀ (x y : AddMonoidAlgebra R M), motive x → motive y → motive (x + y)) →
      (∀ (m : M) (r : R), motive (AddMonoidAlgebra.single m r)) → motive x

Defined in

Mathlib.Algebra.MonoidAlgebra.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

Semiring