Theorems · Definition · ring theory
AddMonoidAlgebra.basis
(R : Type u_7) → (k : Type u_8) → [inst : Semiring k] → Module.Basis R k (AddMonoidAlgebra k R)
The standard basis for an additive monoid algebra.
- Defined in
- Mathlib.Algebra.MonoidAlgebra.Module
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Module.Basisstatement · cited by 1,477
- AddMonoidAlgebrastatement · cited by 649
- AddMonoidAlgebra.coeffLinearEquivproof · cited by 15
Cited by3
Results whose statement or proof uses this declaration.
- LieAlgebra.LoopAlgebra.toFinsuppproof · cited by 3
- LieAlgebra.LoopAlgebra.toFinsupp_symm_singleproof · cited by 0
- AddMonoidAlgebra.basis_applystatement · cited by 0