Semifield

📁 Source: Mathlib/Algebra/Order/Floor/Semifield.lean

Statistics

Metric	Count
Definitions evalNatFloor, Semifield	2
Theorems natFloor, natFloor, natFloor, natFloor, ceil_le_mul, ceil_le_two_mul, ceil_lt_mul, ceil_lt_two_mul, div_two_lt_floor, floor_div_eq_div, floor_div_natCast, floor_div_ofNat, mul_lt_floor	13
Total	15

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalNatFloor 📖	CompOp	—

Mathlib.Meta.NormNum.IsInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natFloor 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Nat.floor Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Nat.floor_of_nonpos Int.cast_negOfNat IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing

Mathlib.Meta.NormNum.IsNNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natFloor 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Nat.floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	to_eq Nat.floor_div_eq_div Nat.cast_id

Mathlib.Meta.NormNum.IsNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natFloor 📖	mathematical	Mathlib.Meta.NormNum.IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Nat.instAddMonoidWithOne Nat.floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Nat.floor_natCast

Mathlib.Meta.NormNum.IsRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natFloor 📖	mathematical	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing Field.toDivisionRing	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Nat.floor DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Nat.cast_zero Nat.floor_eq_zero lt_of_le_of_lt Int.cast_negOfNat invOf_eq_inv neg_mul IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toPosMulMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono one_pos IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ceil_le_mul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Preorder.toLE DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast ceil DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	LE.le.eq_or_lt mul_div_cancel₀ ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_ofNat cast_one cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass ceil_le div_le_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono cast_nonneg' LT.lt.le ceil_lt_mul
ceil_le_two_mul 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instAtLeastTwoHAddOfNat	ceil DivisionSemiring.toSemiring Semifield.toDivisionSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	instAtLeastTwoHAddOfNat ceil_le_mul one_lt_two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat cast_one ceil_one one_div Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul
ceil_lt_mul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast ceil DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	le_total mono_cast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass ceil_le_ceil div_lt_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_trans Mathlib.Meta.Positivity.pos_of_isNat instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_ofNat cast_one ceil_lt_add_one LE.le.trans' le_of_lt inv_pos_of_pos sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add mul_inv_cancel₀ ne_of_gt add_le_add_right mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono sub_one_mul add_sub_cancel
ceil_lt_two_mul 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instAtLeastTwoHAddOfNat	ceil DivisionSemiring.toSemiring Semifield.toDivisionSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	instAtLeastTwoHAddOfNat ceil_lt_mul one_lt_two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat cast_one ceil_one one_div Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul
div_two_lt_floor 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	Preorder.toLT DivInvMonoid.toDiv DivisionRing.toDivInvMonoid instOfNatAtLeastTwo AddMonoidWithOne.toNatCast instAtLeastTwoHAddOfNat floor DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	instAtLeastTwoHAddOfNat div_eq_inv_mul mul_lt_floor Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat cast_zero Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.instAtLeastTwo cast_one Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat ceil_one
floor_div_eq_div 📖	mathematical	—	floor DivisionSemiring.toSemiring Semifield.toDivisionSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	floor_natCast floor_div_natCast
floor_div_natCast 📖	mathematical	—	floor DivisionSemiring.toSemiring Semifield.toDivisionSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	cast_zero div_zero floor_zero div_mul_cancel₀ ne_of_gt cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero mul_cast_floor_div_cancel
floor_div_ofNat 📖	mathematical	—	floor DivisionSemiring.toSemiring Semifield.toDivisionSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	floor_div_natCast
mul_lt_floor 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Preorder.toLE AddMonoidWithOne.toNatCast ceil DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivInvMonoid.toDiv DivisionRing.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib floor	—	mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono lt_floor_add_one mul_add_one Distrib.leftDistribClass le_sub_iff_add_le' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing one_sub_mul div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le ceil_le le_floor

(root)

Definitions

Name	Category	Theorems
Semifield 📖	CompData	—

---

← Back to Index