Theorems · Inductive type · ring theory
NonUnitalNonAssocSemiring
Type u → Type u
A not-necessarily-unital, not-necessarily-associative semiring. See CommutatorRing and the
documentation thereof in case you need a NonUnitalNonAssocSemiring instance on a Lie ring
or a Lie algebra.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 1,081 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by1,422
Results whose statement or proof uses this declaration.
- StarRingstatement · cited by 1,686
- IsTopologicalSemiringstatement · cited by 442
- Matrix.mulVecstatement and proof · cited by 267
- NonUnitalSubalgebrastatement · cited by 215
- NonUnitalStarAlgHomstatement · cited by 208
- NonUnitalSubsemiringstatement · cited by 201
- NonUnitalStarSubalgebrastatement · cited by 196
- Finset.mul_sumstatement and proof · cited by 196
- NonUnitalRingHomstatement · cited by 157
- Matrix.vecMulstatement and proof · cited by 148
- NonUnitalAlgHomstatement · cited by 148
- Finset.sum_mulstatement and proof · cited by 112
Showing the 200 most cited of 1,422.