Theorems · Inductive type · ring theory
NonUnitalCommSemiring
Type u → Type u
A non-unital commutative semiring is a NonUnitalSemiring with commutative multiplication.
In other words, it is a type with the following structures: additive commutative monoid
(AddCommMonoid), commutative semigroup (CommSemigroup), distributive laws (Distrib), and
multiplication by zero law (MulZeroClass).
- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 0 from the axioms · 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 by46
Results whose statement or proof uses this declaration.
- Matrix.vecMul_transposestatement and proof · cited by 8
- NonUnitalSubsemiring.sumSqstatement and proof · cited by 6
- Matrix.dotProduct_transpose_mulVecstatement and proof · cited by 3
- Matrix.mulVec_transposestatement and proof · cited by 3
- RingEquiv.toOppositestatement and proof · cited by 3
- Matrix.trace_mul_cyclestatement and proof · cited by 2
- Matrix.mulVec_consstatement and proof · cited by 1
- NonUnitalSubsemiring.sumSq_toAddSubmonoidstatement and proof · cited by 1
- NonUnitalCommSemiring.casesOnstatement and proof · cited by 1
- NonUnitalCommSemiring.extstatement and proof · cited by 1
- NonUnitalCommSemiring.toNonUnitalSemiring_injectivestatement and proof · cited by 1
- NonUnitalSubsemiring.closure_isSquarestatement and proof · cited by 1