Theorems · Inductive type · commutative algebra

PolynomialLaw

(R : Type u) →
  [inst : CommSemiring R] →
    (M : Type u_1) →
      [inst_1 : AddCommMonoid M] →
        [Module R M] → (N : Type u_2) → [inst_3 : AddCommMonoid N] → [Module R N] → Type (max (max (u + 1) u_1) u_2)

A polynomial law M →ₚₗ[R] N between R-modules is a functorial family of maps S ⊗[R] M → S ⊗[R] N, for all R-algebras S. For universe reasons, S has to be restricted to the same universe as R.

Defined in

Mathlib.RingTheory.PolynomialLaw.Basic

Cited by

37 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule