Theorems · Inductive type · ring theory
AddMonoidAlgebra
(R : Type u_8) → Type u_9 → [Semiring R] → Type (max u_8 u_9)
The additive monoid algebra over a semiring R generated by the additive monoid M.
It is the type of finite formal R-linear combinations of terms of M,
endowed with the convolution product.
- Defined in
- Mathlib.Algebra.MonoidAlgebra.Defs
- Cited by
- 649 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
Cited by766
Results whose statement or proof uses this declaration.
- MvPolynomialproof · cited by 2,140
- Polynomial.coeffproof · cited by 1,045
- MvPolynomial.Cproof · cited by 400
- AddMonoidAlgebra.coeffstatement and proof · cited by 365
- AddMonoidAlgebra.singlestatement · cited by 250
- Polynomial.supportproof · cited by 237
- LaurentPolynomialproof · cited by 98
- AddMonoidAlgebra.extstatement and proof · cited by 90
- Polynomial.coeff_addproof · cited by 77
- Polynomial.toFinsuppstatement · cited by 64
- Polynomial.coeff_C_mulproof · cited by 55
- AddMonoidAlgebra.supDegreestatement and proof · cited by 49
Showing the 200 most cited of 766.