Semiring

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

Statistics

Metric	Count
Definitions	0
Theorems abs_ceil_sub_le, abs_floor_sub_le, abs_sub_ceil_le, abs_sub_floor_le, add_one_le_ceil_iff, cast_mul_floor_div_cancel, ceil_add_le, ceil_add_natCast, ceil_add_ofNat, ceil_add_one, ceil_congr, ceil_eq_iff, ceil_eq_zero, ceil_intCast, ceil_le_ceil, ceil_le_floor_add_one, ceil_lt_add_one, ceil_mono, ceil_natCast, ceil_ofNat, ceil_one, ceil_sub_natCast, ceil_sub_ofNat, ceil_sub_one, ceil_zero, floor_add_natCast, floor_add_ofNat, floor_add_one, floor_congr, floor_eq_iff, floor_eq_iff', floor_eq_on_Ico, floor_eq_on_Ico', floor_eq_zero, floor_le, floor_le_ceil, floor_le_floor, floor_le_of_le, floor_le_one_of_le_one, floor_lt, floor_lt', floor_lt_ceil_of_lt_of_pos, floor_lt_one, floor_mono, floor_natCast, floor_ofNat, floor_of_nonpos, floor_one, floor_pos, floor_sub_natCast, floor_sub_ofNat, floor_sub_one, floor_zero, le_ceil, le_floor_iff', le_of_ceil_le, lt_floor_add_one, lt_of_ceil_lt, lt_of_floor_lt, lt_of_lt_floor, lt_one_of_floor_lt_one, lt_succ_floor, map_ceil, map_floor, mul_cast_floor_div_cancel, one_le_ceil_iff, one_le_floor_iff, pos_of_floor_pos, preimage_Icc, preimage_Ici, preimage_Ico, preimage_Iic, preimage_Iio, preimage_Ioc, preimage_Ioi, preimage_Ioo, preimage_ceil_of_ne_zero, preimage_ceil_zero, preimage_floor_of_ne_zero, preimage_floor_zero, sub_one_lt_floor, subsingleton_floorSemiring	82
Total	82

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_ceil_sub_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne ceil Ring.toSemiring AddMonoidWithOne.toOne	—	abs_sub_ceil_le abs_sub_comm
abs_floor_sub_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne floor Ring.toSemiring AddMonoidWithOne.toOne	—	abs_sub_floor_le abs_sub_comm
abs_sub_ceil_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne ceil Ring.toSemiring AddMonoidWithOne.toOne	—	abs_le IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedAddMonoid.toAddLeftMono LT.lt.le ceil_lt_add_one AddGroup.toOrderedSub covariant_swap_add_of_covariant_add LE.le.trans le_ceil le_add_of_nonneg_left zero_le_one IsStrictOrderedRing.toZeroLEOneClass
abs_sub_floor_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne floor Ring.toSemiring AddMonoidWithOne.toOne	—	abs_le IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsOrderedAddMonoid.toAddLeftMono LE.le.trans floor_le le_add_of_nonneg_right zero_le_one IsStrictOrderedRing.toZeroLEOneClass AddGroup.toOrderedSub covariant_swap_add_of_covariant_add add_comm LT.lt.le lt_floor_add_one
add_one_le_ceil_iff 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	lt_ceil
cast_mul_floor_div_cancel 📖	mathematical	—	floor CommSemiring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mul_comm mul_cast_floor_div_cancel
ceil_add_le 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	ceil_le cast_add add_le_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add le_ceil
ceil_add_natCast 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	ceil Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	eq_of_forall_ge_iff Mathlib.Tactic.Contrapose.contrapose_iff₁ lt_ceil le_or_gt ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd cast_add add_comm add_lt_add_iff_right IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le AddRightCancelSemigroup.toIsRightCancelAdd instIsOrderedAddMonoid lt_add_of_nonneg_of_lt cast_lt IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero
ceil_add_ofNat 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	ceil Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	ceil_add_natCast
ceil_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	ceil Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	cast_one ceil_add_natCast
ceil_congr 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	ceil	—	LE.le.antisymm ceil_le le_ceil
ceil_eq_iff 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Preorder.toLE	—	ceil_le not_le tsub_lt_iff_right CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le pos_iff_ne_zero le_antisymm_iff
ceil_eq_zero 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	ceil_le cast_zero
ceil_intCast 📖	mathematical	—	ceil Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	eq_of_forall_ge_iff Int.cast_natCast IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
ceil_le_ceil 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	ceil	—	ceil_mono
ceil_le_floor_add_one 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder floor	—	ceil_le cast_add cast_one LT.lt.le lt_floor_add_one
ceil_lt_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Preorder.toLT AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne ceil Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne	—	lt_ceil LT.lt.trans_le Eq.ge ceil_add_one
ceil_mono 📖	mathematical	—	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instPreorder ceil	—	GaloisConnection.monotone_l gc_ceil_coe
ceil_natCast 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	eq_of_forall_ge_iff ceil_le cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero
ceil_ofNat 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	ceil_natCast
ceil_one 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	cast_one ceil_natCast
ceil_sub_natCast 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	le_total ceil_eq_zero tsub_nonpos_of_le tsub_eq_zero_iff_le instCanonicallyOrderedAdd instOrderedSub ceil_le eq_tsub_of_add_eq IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid ceil_add_natCast le_tsub_of_add_le_left IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Eq.trans_le add_zero tsub_add_cancel_of_le
ceil_sub_ofNat 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	ceil_sub_natCast
ceil_sub_one 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	cast_one ceil_sub_natCast
ceil_zero 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	cast_zero ceil_natCast
floor_add_natCast 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	floor Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	eq_of_forall_le_iff le_floor_iff add_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing cast_nonneg le_total ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd cast_add add_comm add_le_add_iff_right covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT IsCancelAdd.toIsRightCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le instIsOrderedAddMonoid AddRightCancelSemigroup.toIsRightCancelAdd add_left_comm le_add_of_nonneg_right LE.le.trans le_self_add
floor_add_ofNat 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	floor Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	floor_add_natCast
floor_add_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	floor Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	cast_one floor_add_natCast
floor_congr 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	floor	—	cast_zero lt_or_ge floor_of_nonpos LT.lt.le le_of_not_ge Iff.not LT.lt.not_ge LE.le.antisymm le_floor IsStrictOrderedRing.toIsOrderedRing floor_le
floor_eq_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	floor AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLT Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne	—	le_floor_iff cast_one cast_add floor_lt le_antisymm_iff
floor_eq_iff' 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Preorder.toLT Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne	—	le_floor_iff' cast_one cast_add floor_lt' le_antisymm_iff
floor_eq_on_Ico 📖	mathematical	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne	floor	—	floor_eq_iff LE.le.trans cast_nonneg IsStrictOrderedRing.toIsOrderedRing
floor_eq_on_Ico' 📖	mathematical	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne	floor	—	IsStrictOrderedRing.toCharZero floor_eq_on_Ico
floor_eq_zero 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	cast_one floor_lt'
floor_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne floor	—	le_floor_iff le_rfl
floor_le_ceil 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ceil	—	le_total floor_of_nonpos cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero LE.le.trans floor_le le_ceil
floor_le_floor 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	floor	—	floor_mono
floor_le_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	floor	—	le_imp_le_iff_lt_imp_lt lt_of_lt_floor
floor_le_one_of_le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	floor	—	floor_le_of_le LE.le.trans_eq cast_one
floor_lt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	floor Preorder.toLT AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	lt_iff_lt_of_le_iff_le le_floor_iff
floor_lt' 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	lt_iff_lt_of_le_iff_le le_floor_iff'
floor_lt_ceil_of_lt_of_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	floor ceil	—	le_or_gt floor_lt LT.lt.trans_le le_ceil floor_of_nonpos LT.lt.le lt_ceil cast_zero
floor_lt_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	floor Preorder.toLT AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	floor_lt cast_one
floor_mono 📖	mathematical	—	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instPreorder floor	—	le_total floor_of_nonpos le_floor IsStrictOrderedRing.toIsOrderedRing LE.le.trans floor_le
floor_natCast 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	eq_of_forall_le_iff le_floor_iff cast_nonneg IsStrictOrderedRing.toIsOrderedRing cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero
floor_ofNat 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	floor_natCast
floor_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	floor	—	LE.le.lt_or_eq FloorSemiring.floor_of_neg floor_zero
floor_one 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	cast_one floor_natCast
floor_pos 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	zero_add le_floor_iff' cast_one
floor_sub_natCast 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	le_total floor_of_nonpos tsub_nonpos_of_le LE.le.trans cast_nonneg IsStrictOrderedRing.toIsOrderedRing zero_tsub instCanonicallyOrderedAdd instOrderedSub tsub_eq_zero_iff_le cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero floor_le eq_tsub_iff_add_eq_of_le CanonicallyOrderedAdd.toExistsAddOfLE instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le le_floor floor_add_natCast le_tsub_of_add_le_left IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Eq.trans_le add_zero tsub_add_cancel_of_le
floor_sub_ofNat 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	floor_sub_natCast
floor_sub_one 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	cast_one floor_sub_natCast
floor_zero 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	cast_zero floor_natCast
le_ceil 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring ceil	—	ceil_le le_rfl
le_floor_iff' 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	le_total floor_of_nonpos LT.lt.not_ge not_le_of_gt LE.le.trans_lt cast_pos IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero le_floor_iff
le_of_ceil_le 📖	mathematical	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	LE.le.trans le_ceil cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero
lt_floor_add_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne floor AddMonoidWithOne.toOne	—	cast_add cast_one lt_succ_floor
lt_of_ceil_lt 📖	mathematical	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	LE.le.trans_lt le_ceil cast_lt IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero
lt_of_floor_lt 📖	mathematical	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	lt_of_not_ge LE.le.not_gt le_floor IsStrictOrderedRing.toIsOrderedRing
lt_of_lt_floor 📖	mathematical	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	LT.lt.trans_le cast_lt IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero floor_le LT.lt.le pos_of_floor_pos LE.le.trans_lt
lt_one_of_floor_lt_one 📖	mathematical	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	cast_one lt_of_floor_lt
lt_succ_floor 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring floor	—	lt_of_floor_lt
map_ceil 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe	ceil	—	ceil_congr map_natCast StrictMono.le_iff_le
map_floor 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe	floor	—	floor_congr map_natCast StrictMono.le_iff_le
mul_cast_floor_div_cancel 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_total floor_of_nonpos mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing cast_nonneg eq_of_forall_le_iff le_floor_iff mul_nonneg IsOrderedRing.toPosMulMono cast_nonneg' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass cast_mul mul_le_mul_iff_of_pos_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono cast_pos' NeZero.charZero_one IsStrictOrderedRing.toCharZero
one_le_ceil_iff 📖	mathematical	—	ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	zero_add add_one_le_ceil_iff cast_zero
one_le_floor_iff 📖	mathematical	—	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	cast_one le_floor_iff' one_ne_zero
pos_of_floor_pos 📖	mathematical	floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	le_or_gt lt_irrefl floor_of_nonpos
preimage_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Set.preimage AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Icc instPreorder ceil floor	—	Set.ext
preimage_Ici 📖	mathematical	—	Set.preimage AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instPreorder ceil	—	Set.ext
preimage_Ico 📖	mathematical	—	Set.preimage AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instPreorder ceil	—	Set.ext
preimage_Iic 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Set.preimage AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Iic instPreorder floor	—	Set.ext
preimage_Iio 📖	mathematical	—	Set.preimage AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instPreorder ceil	—	Set.ext
preimage_Ioc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Set.preimage AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Ioc instPreorder floor	—	Set.ext
preimage_Ioi 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Set.preimage AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Ioi instPreorder floor	—	Set.ext
preimage_Ioo 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Set.preimage AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.Ioo instPreorder floor ceil	—	Set.ext
preimage_ceil_of_ne_zero 📖	mathematical	—	Set.preimage ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instSingletonSet Set.Ioc PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Set.ext ceil_eq_iff
preimage_ceil_zero 📖	mathematical	—	Set.preimage ceil SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instSingletonSet Set.Iic PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Set.ext ceil_eq_zero
preimage_floor_of_ne_zero 📖	mathematical	—	Set.preimage floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instSingletonSet Set.Ico PartialOrder.toPreorder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne	—	Set.ext floor_eq_iff'
preimage_floor_zero 📖	mathematical	—	Set.preimage floor SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instSingletonSet Set.Iio PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Set.ext floor_eq_zero
sub_one_lt_floor 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toNatCast floor Ring.toSemiring	—	sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_floor_add_one

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subsingleton_floorSemiring 📖	mathematical	—	FloorSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	GaloisConnection.l_unique FloorSemiring.gc_ceil lt_or_ge FloorSemiring.floor_of_neg eq_of_forall_le_iff FloorSemiring.gc_floor

---

← Back to Index