Theorems · Inductive type · field theory
DivisionSemiring
Type u_2 → Type u_2
A DivisionSemiring is a Semiring with multiplicative inverses for nonzero elements.
An instance of DivisionSemiring K includes maps nnratCast : ℚ≥0 → K and nnqsmul : ℚ≥0 → K → K.
Those two fields are needed to implement the DivisionSemiring K → Algebra ℚ≥0 K instance since we
need to control the specific definitions for some special cases of K (in particular K = ℚ≥0
itself). See also note [forgetful inheritance].
If the division semiring has positive characteristic p, our division by zero convention forces
nnratCast (1 / p) = 1 / 0 = 0.
- Defined in
- Mathlib.Algebra.Field.Defs
- Cited by
- 216 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 by234
Results whose statement or proof uses this declaration.
- add_divstatement and proof · cited by 89
- add_halvesstatement and proof · cited by 78
- uniqueDiffOn_univstatement and proof · cited by 66
- NNRat.cast_natCaststatement and proof · cited by 31
- birkhoffAveragestatement and proof · cited by 25
- tsum_mul_leftstatement and proof · cited by 21
- Finset.sum_divstatement and proof · cited by 20
- Submodule.smul_mem_iffstatement and proof · cited by 19
- add_self_div_twostatement and proof · cited by 18
- HasSum.div_conststatement and proof · cited by 18
- NNRat.cast_defstatement and proof · cited by 17
- uniqueDiffWithinAt_univstatement and proof · cited by 16
Showing the 200 most cited of 234.