Field

📁 Source: Mathlib/Algebra/Order/Nonneg/Field.lean

Statistics

Metric	Count
Definitions div, instNNRatCast, instNNRatSMul, inv, linearOrderedCommGroupWithZero, semifield, unitsEquivPos, zpow	8
Theorems cast_nonneg, coe_div, coe_inv, coe_nnqsmul, coe_nnratCast, coe_zpow, inv_mk, mk_div_mk, mk_nnqsmul, mk_nnratCast, mk_zpow, unitsEquivPos_apply_coe, val_inv_unitsEquivPos_symm_apply_coe, val_unitsEquivPos_symm_apply_coe, nnqsmul_nonneg	15
Total	23

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring cast DivisionSemiring.toNNRatCast	—	cast_def div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing

Nonneg

Definitions

Name	Category	Theorems
div 📖	CompOp	2 math math: mk_div_mk, coe_div
instNNRatCast 📖	CompOp	3 math math: mk_nnratCast, coe_nnratCast, NNRat.Nonneg.coe_ofScientific
instNNRatSMul 📖	CompOp	1 math math: coe_nnqsmul
inv 📖	CompOp	2 math math: inv_mk, coe_inv
linearOrderedCommGroupWithZero 📖	CompOp	—
semifield 📖	CompOp	—
unitsEquivPos 📖	CompOp	3 math math: val_unitsEquivPos_symm_apply_coe, unitsEquivPos_apply_coe, val_inv_unitsEquivPos_symm_apply_coe
zpow 📖	CompOp	2 math math: mk_zpow, coe_zpow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_div 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring div DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	—
coe_inv 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	—
coe_nnqsmul 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat instNNRatSMul NNRat.smulDivisionSemiring	—	—
coe_nnratCast 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.cast instNNRatCast DivisionSemiring.toNNRatCast	—	—
coe_zpow 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring zpow DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	—
inv_mk 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero GroupWithZero.toDivisionMonoid inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE MulZeroClass.toMul IsStrictOrderedRing.toPosMulStrictMono	—	—
mk_div_mk 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	div DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE MulZeroClass.toMul IsStrictOrderedRing.toPosMulStrictMono	—	—
mk_nnqsmul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	NNRat NNRat.smulDivisionSemiring	—	—
mk_nnratCast 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.cast DivisionSemiring.toNNRatCast NNRat.cast_nonneg instNNRatCast	—	NNRat.cast_nonneg
mk_zpow 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	zpow DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero zpow_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE MulZeroClass.toMul IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass	—	—
unitsEquivPos_apply_coe 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring DFunLike.coe MulEquiv Units Preorder.toLE MonoidWithZero.toMonoid monoidWithZero IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Units.instMul Positive.instMulSubtypeLtOfNat_mathlib EquivLike.toFunLike MulEquiv.instEquivLike unitsEquivPos Units.val	—	IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono
val_inv_unitsEquivPos_symm_apply_coe 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Units.val MonoidWithZero.toMonoid monoidWithZero Units Units.instInv DFunLike.coe MulEquiv Preorder.toLT IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Positive.instMulSubtypeLtOfNat_mathlib Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm unitsEquivPos InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono
val_unitsEquivPos_symm_apply_coe 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Units.val MonoidWithZero.toMonoid monoidWithZero DFunLike.coe MulEquiv Preorder.toLT Units IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono NonUnitalNonAssocSemiring.toAddCommMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono Positive.instMulSubtypeLtOfNat_mathlib Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm unitsEquivPos	—	IsStrictOrderedRing.toZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnqsmul_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	NNRat NNRat.smulDivisionSemiring	—	NNRat.smul_def mul_nonneg IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing NNRat.cast_nonneg

---

← Back to Index