Theorems · Inductive type · ring theory
MonoidAlgebra
(R : Type u_8) → Type u_9 → [Semiring R] → Type (max u_8 u_9)
The monoid algebra over a semiring R generated by the 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
- 590 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 by744
Results whose statement or proof uses this declaration.
- MonoidAlgebra.singlestatement · cited by 253
- MonoidAlgebra.coeffstatement and proof · cited by 224
- MonoidAlgebra.extstatement and proof · cited by 78
- Representation.leftRegularstatement · cited by 39
- Representation.linearizestatement · cited by 36
- MonoidAlgebra.coeffLinearEquivstatement · cited by 34
- MonoidAlgebra.ofstatement and proof · cited by 30
- MonoidAlgebra.mapRingHomstatement · cited by 27
- MonoidAlgebra.of_applystatement · cited by 26
- MonoidAlgebra.lsinglestatement · cited by 25
- MonoidAlgebra.coeffLinearEquiv_applystatement and proof · cited by 22
- MonoidAlgebra.lhom_ext'statement and proof · cited by 21
Showing the 200 most cited of 744.