Theorems · Theorem · ring theory

TensorAlgebra.induction

∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {C : TensorAlgebra R M → Prop},
  (∀ (r : R), C ((algebraMap R (TensorAlgebra R M)) r)) →
    (∀ (x : M), C ((TensorAlgebra.ι R) x)) →
      (∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)) →
        (∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)) → ∀ (a : TensorAlgebra R M), C a

If C holds for the algebraMap of r : R into TensorAlgebra R M, the ι of x : M, and is preserved under addition and multiplication, then it holds for all of TensorAlgebra R M.

Defined in

Mathlib.LinearAlgebra.TensorAlgebra.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule