Floor

📁 Source: Mathlib/Data/Rat/Floor.lean

Statistics

Metric	Count
Definitions evalIntCeil, evalIntFloor, evalIntFract, evalRound, instFloorRing	5
Theorems mod_nat_eq_sub_mul_floor_rat_div, coprime_sub_mul_floor_rat_div_of_coprime, isInt_round, cast_fract, ceil_cast, ceil_def', ceil_intCast_div_natCast, ceil_natCast_div_natCast, den_intFract, floor_cast, floor_def', floor_intCast_div_natCast, floor_natCast_div_natCast, fract_inv_num_lt_num_of_pos, isInt_intCeil, isInt_intCeil_ofIsRat_neg, isInt_intFloor, isInt_intFloor_ofIsRat_neg, isInt_round, isNNRat_intFract_of_isNNRat, isNat_intCeil, isNat_intCeil_ofIsNNRat, isNat_intFloor, isNat_intFloor_ofIsNNRat, isNat_intFract_of_isInt, isNat_intFract_of_isNat, isNat_round, isRat_intFract_of_isRat_negOfNat, le_floor, natFloor_natCast_div_natCast, num_lt_succ_floor_mul_den, round_cast	32
Total	37

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mod_nat_eq_sub_mul_floor_rat_div 📖	mathematical	—	floor DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	Rat.floor_intCast_div_natCast

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprime_sub_mul_floor_rat_div_of_coprime 📖	mathematical	—	Int.floor DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing	—	Int.mod_nat_eq_sub_mul_floor_rat_div

Rat

Definitions

Name	Category	Theorems
evalIntCeil 📖	CompOp	—
evalIntFloor 📖	CompOp	—
evalIntFract 📖	CompOp	—
evalRound 📖	CompOp	—
instFloorRing 📖	CompOp	45 math math: num_lt_succ_floor_mul_den, NNRat.coe_floor, GenContFract.IntFractPair.coe_stream_nth_rat_eq, GenContFract.coe_of_h_rat_eq, GenContFract.coe_of_s_rat_eq, cast_fract, ceil_intCast_div_natCast, NNRat.floor_coe, GenContFract.of_terminates_iff_of_rat_terminates, GenContFract.IntFractPair.coe_stream'_rat_eq, GenContFract.IntFractPair.exists_nth_stream_eq_none_of_rat, floor_natCast_div_natCast, round_cast, NNRat.intCeil_cast, floor_cast, GenContFract.IntFractPair.coe_of_rat_eq, GenContFract.coe_of_rat_eq, NNRat.coe_ceil, Nat.Ioc_filter_modEq_card, ceil_natCast_div_natCast, Int.Ioc_filter_modEq_card, GenContFract.IntFractPair.of_inv_fr_num_lt_num_of_pos, Nat.Ico_filter_modEq_card, natFloor_natCast_div_natCast, GaussianInt.div_def, Int.Ico_filter_dvd_card, GenContFract.coe_of_s_get?_rat_eq, fract_inv_num_lt_num_of_pos, den_le_and_le_num_le_of_sub_lt_one_div_den_sq, Nat.coprime_sub_mul_floor_rat_div_of_coprime, NNRat.ceil_coe, floor_def', Int.Ico_filter_modEq_card, Int.Ioc_filter_dvd_eq, ceil_cast, GenContFract.terminates_of_rat, Nat.count_modEq_card_eq_ceil, NNRat.intFloor_cast, den_intFract, Int.mod_nat_eq_sub_mul_floor_rat_div, Int.Ico_filter_dvd_eq, floor_intCast_div_natCast, Int.Ioc_filter_dvd_card, ceil_def', niven_fract_angle_div_pi_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_fract 📖	mathematical	—	DivisionRing.toRatCast Field.toDivisionRing Int.fract DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	cast_sub IsStrictOrderedRing.toCharZero cast_intCast floor_cast
ceil_cast 📖	mathematical	—	Int.ceil DivisionRing.toRing Field.toDivisionRing DivisionRing.toRatCast instDivisionRing linearOrder instFloorRing	—	Int.floor_neg instIsStrictOrderedRing cast_neg floor_cast
ceil_def' 📖	mathematical	—	Int.ceil DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	floor_def' num_neg_eq_neg_num den_neg_eq_den
ceil_intCast_div_natCast 📖	mathematical	—	Int.ceil DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	neg_neg Int.floor_neg instIsStrictOrderedRing neg_div Int.cast_neg floor_intCast_div_natCast
ceil_natCast_div_natCast 📖	mathematical	—	Int.ceil DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	ceil_intCast_div_natCast
den_intFract 📖	mathematical	—	Int.fract DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	sub_intCast_den
floor_cast 📖	mathematical	—	Int.floor DivisionRing.toRing Field.toDivisionRing DivisionRing.toRatCast instDivisionRing linearOrder instFloorRing	—	Int.floor_eq_iff Nat.cast_one Int.cast_one
floor_def' 📖	mathematical	—	Int.floor DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	—
floor_intCast_div_natCast 📖	mathematical	—	Int.floor DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	floor_def' eq_zero_or_pos Nat.instCanonicallyOrderedAdd Nat.cast_zero div_zero Nat.cast_one instCharZero Int.cast_natCast exists_eq_mul_div_num_and_eq_mul_div_den Int.instCharZero LT.lt.ne' pos_of_mul_pos_left MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Int.instIsStrictOrderedRing
floor_natCast_div_natCast 📖	mathematical	—	Int.floor DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	floor_intCast_div_natCast
fract_inv_num_lt_num_of_pos 📖	mathematical	—	Int.fract DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	num_pos LT.lt.le Int.cast_natCast num_lt_succ_floor_mul_den one_mul right_distrib Distrib.rightDistribClass sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono instCharZero num_div_eq_of_coprime den_div_eq_of_coprime Int.instCharZero mul_comm Nat.coprime_sub_mul_floor_rat_div_of_coprime Nat.cast_natAbs abs_of_nonneg Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Int.cast_pos IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing IsOrderedRing.toZeroLEOneClass NeZero.one nontrivial Mathlib.Meta.Positivity.num_pos_of_pos Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'
isInt_intCeil 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Int.instRing Int.ceil	—	Int.ceil_intCast
isInt_intCeil_ofIsRat_neg 📖	mathematical	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing Field.toDivisionRing	Mathlib.Meta.NormNum.IsInt Int.instRing Int.ceil	—	invOf_eq_inv floor_natCast_div_natCast neg_neg ceil_intCast_div_natCast ceil_cast cast_div IsStrictOrderedRing.toCharZero cast_intCast cast_natCast
isInt_intFloor 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Int.instRing Int.floor	—	Int.floor_intCast
isInt_intFloor_ofIsRat_neg 📖	mathematical	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing Field.toDivisionRing	Mathlib.Meta.NormNum.IsInt Int.instRing Int.floor	—	invOf_eq_inv ceil_intCast_div_natCast Int.cast_natCast Int.ceil_nonneg instIsStrictOrderedRing div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing neg_neg floor_intCast_div_natCast floor_cast cast_div IsStrictOrderedRing.toCharZero cast_intCast cast_natCast
isInt_round 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Int.instRing round	—	round_intCast
isNNRat_intFract_of_isNNRat 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Int.fract DivisionRing.toRing Field.toDivisionRing	—	invOf_eq_inv Int.fract_div_natCast_eq_div_natCast_mod
isNat_intCeil 📖	mathematical	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Int.instRing Int.ceil	—	Int.ceil_natCast
isNat_intCeil_ofIsNNRat 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing Int.ceil DivisionRing.toRing Field.toDivisionRing	—	invOf_eq_inv ceil_intCast_div_natCast ceil_cast cast_div IsStrictOrderedRing.toCharZero cast_intCast cast_natCast Int.cast_natCast Int.ceil_nonneg div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing
isNat_intFloor 📖	mathematical	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Int.instRing Int.floor	—	Int.floor_natCast
isNat_intFloor_ofIsNNRat 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing Int.floor DivisionRing.toRing Field.toDivisionRing	—	invOf_eq_inv floor_natCast_div_natCast floor_cast cast_div IsStrictOrderedRing.toCharZero cast_natCast
isNat_intFract_of_isInt 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.fract	—	Int.fract_intCast Nat.cast_zero
isNat_intFract_of_isNat 📖	mathematical	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Int.fract	—	Int.fract_natCast Nat.cast_zero
isNat_round 📖	mathematical	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Int.instRing round	—	round_natCast
isRat_intFract_of_isRat_negOfNat 📖	mathematical	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing Field.toDivisionRing	Int.fract	—	invOf_eq_inv Int.fract_div_intCast_eq_div_intCast_mod
le_floor 📖	—	—	—	—	intCast_eq_divInt divInt_le_divInt zero_lt_one Int.instZeroLEOneClass mul_one
natFloor_natCast_div_natCast 📖	mathematical	—	Nat.floor semiring instPartialOrder FloorRing.toFloorSemiring DivisionRing.toRing instDivisionRing linearOrder instIsStrictOrderedRing instFloorRing	—	instIsStrictOrderedRing Int.natCast_floor_eq_floor div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_nonneg' instAddLeftMono instZeroLEOneClass floor_intCast_div_natCast
num_lt_succ_floor_mul_den 📖	mathematical	—	Int.floor DivisionRing.toRing instDivisionRing linearOrder instFloorRing	—	Int.fract_lt_one instIsStrictOrderedRing zero_add lt_sub_iff_add_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add instAddLeftMono mul_pos IsStrictOrderedRing.toPosMulStrictMono Nat.cast_zero instZeroLEOneClass instCharZero pos sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sub_self Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.zero_mul add_mul Distrib.rightDistribClass mul_den_eq_num eq_sub_of_add_eq Int.floor_add_fract Nat.cast_one Int.cast_one Int.cast_natCast NeZero.charZero_one
round_cast 📖	mathematical	—	round DivisionRing.toRing Field.toDivisionRing DivisionRing.toRatCast instDivisionRing linearOrder instFloorRing	—	Nat.instAtLeastTwoHAddOfNat one_div cast_add IsStrictOrderedRing.toCharZero cast_inv cast_ofNat round_eq instIsStrictOrderedRing floor_cast

Rat.IsRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInt_round 📖	mathematical	round DivisionRing.toRing Rat.instDivisionRing Rat.linearOrder Rat.instFloorRing Mathlib.Meta.NormNum.IsRat Field.toDivisionRing	Mathlib.Meta.NormNum.IsInt Int.instRing	—	invOf_eq_inv div_eq_mul_inv Int.cast_natCast IsStrictOrderedRing.toCharZero Rat.round_cast Rat.instCharZero Rat.instIsStrictOrderedRing

---

← Back to Index