Structures · Algebra

DivisionRing

A DivisionRing is a Ring with multiplicative inverses for nonzero elements. An instance of DivisionRing K includes maps ratCast : ℚ → K and qsmul : ℚ → K → K. Those two fields are needed to implement the DivisionRing K → Algebra ℚ K instance since we need to control the specific definitions for some special cases of K (in particular K = ℚ itself). See also note [forgetful inheritance]. Similarly, there are maps nnratCast ℚ≥0 → K and nnqsmul : ℚ≥0 → K → K to implement the DivisionSemiring K → Algebra ℚ≥0 K instance. If the division ring has positive characteristic p, our division by zero convention forces ratCast (1 / p) = 1 / 0 = 0.

Defined in

Mathlib.Algebra.Field.Defs

Shape

One type argument · adds div_eq_mul_inv, zpow_zero', zpow_succ', zpow_neg', mul_inv_cancel, inv_zero, nnratCast_def, nnqsmul, nnqsmul_def, ratCast_def, qsmul, qsmul_def