Theorems · Definition · ring theory
MonoidAlgebra.single
{R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → R → MonoidAlgebra R MMonoidAlgebra.single m r for m : M, r : R is the element rm : R[M].
- Defined in
- Mathlib.Algebra.MonoidAlgebra.Defs
- Cited by
- 253 results in Mathlib
- Foundations
- Depth 60 from the axioms, rests on 864 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Finsupp.singleproof · cited by 943
- MonoidAlgebrastatement · cited by 590
Cited by266
Results whose statement or proof uses this declaration.
- MonoidAlgebra.of_applystatement · cited by 26
- MonoidAlgebra.single_mul_singlestatement and proof · cited by 14
- MonoidAlgebra.mapDomainLinearMap_singlestatement and proof · cited by 13
- MonoidAlgebra.mapDomain_singlestatement and proof · cited by 12
- Representation.asAlgebraHom_singlestatement · cited by 11
- Representation.IndV.mkproof · cited by 11
- MonoidAlgebra.coeff_mulproof · cited by 11
- MonoidAlgebra.mapRingHom_singlestatement and proof · cited by 11
- MonoidAlgebra.smul_singlestatement · cited by 10
- MonoidAlgebra.tensorEquiv_single_tmul_singlestatement and proof · cited by 8
- MonoidAlgebra.algHom_extstatement and proof · cited by 7
- MonoidAlgebra.mul_defstatement · cited by 7
Showing the 200 most cited of 266.