Theorems · Inductive type · field theory

Semifield

Type u_2 → Type u_2

A Semifield is a CommSemiring with multiplicative inverses for nonzero elements. An instance of Semifield 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 semifield has positive characteristic p, our division by zero convention forces nnratCast (1 / p) = 1 / 0 = 0.

Defined in

Mathlib.Algebra.Field.Defs

Cited by

439 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms