Round

📁 Source: Mathlib/Algebra/Order/Round.lean

Statistics

Metric	Count
Definitions round	1
Theorems map_round, abs_sub_round, abs_sub_round_div_natCast_eq, abs_sub_round_eq_min, round_add_intCast, round_add_natCast, round_add_ofNat, round_add_one, round_eq, round_eq_div, round_eq_half_ceil_two_mul, round_eq_iff, round_eq_zero_iff, round_intCast, round_intCast_add, round_le, round_le_add_half, round_natCast, round_natCast_add, round_neg_two_inv, round_ofNat, round_ofNat_add, round_one, round_sub_intCast, round_sub_natCast, round_sub_ofNat, round_sub_one, round_two_inv, round_zero, sub_half_lt_round	30
Total	31

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_round 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe	round DivisionRing.toRing Field.toDivisionRing	—	Nat.instAtLeastTwoHAddOfNat round_eq map_floor map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass one_div map_inv₀ RingHomClass.toMonoidWithZeroHomClass map_ofNat

(root)

Definitions

Name	Category	Theorems
round 📖	CompOp	44 math math: abs_sub_round, round_neg_two_inv, round_add_natCast, round_two_inv, Real.round_exp_one_eq_three, round_sub_intCast, round_sub_one, round_eq_div, GaussianInt.toComplex_div_re, round_natCast, round_intCast_add, sub_half_lt_round, round_add_one, round_add_intCast, abs_sub_round_div_natCast_eq, Rat.round_cast, round_natCast_add, GaussianInt.toComplex_im_div, Real.exists_nat_abs_mul_sub_round_le, round_le, abs_sub_round_eq_min, GaussianInt.div_def, round_eq, round_intCast, round_sub_ofNat, GaussianInt.toComplex_re_div, round_eq_zero_iff, round_ofNat_add, round_add_ofNat, Rat.isInt_round, UnitAddCircle.norm_eq, Int.map_round, Rat.isNat_round, round_le_add_half, round_eq_half_ceil_two_mul, round_eq_iff, round_sub_natCast, round_one, AddCircle.norm_eq, round_zero, round_ofNat, AddCircle.norm_eq', Real.round_pi_eq_three, GaussianInt.toComplex_div_im

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_sub_round 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toIntCast round DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat round_eq abs_sub_le_iff IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Int.floor_le Int.lt_floor_add_one le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt 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_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le
abs_sub_round_div_natCast_eq 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne AddGroupWithOne.toIntCast round	—	Nat.cast_zero div_zero round_zero Int.cast_zero sub_self abs_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub inf_of_le_right IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero abs_sub_round_eq_min Nat.cast_min min_div_div_right LT.lt.le Int.fract_div_natCast_eq_div_natCast_mod Nat.cast_sub sub_div div_self LT.lt.ne'
abs_sub_round_eq_min 📖	mathematical	—	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toIntCast round SemilatticeInf.toMin Lattice.toSemilatticeInf Int.fract AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	min_def_lt two_mul AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_or_ge Int.self_sub_floor Int.abs_fract lt_of_lt_of_le zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero tsub_le_iff_left Nat.instAtLeastTwoHAddOfNat IsStrictOrderedRing.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE not_lt abs_sub_comm Int.ceil_sub_self_eq LT.lt.ne Int.abs_one_sub_fract
round_add_intCast 📖	mathematical	—	round Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	round.eq_1 Int.fract_add_intCast Int.floor_add_intCast Int.ceil_add_intCast apply_ite₂
round_add_natCast 📖	mathematical	—	round Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Int.cast_natCast round_add_intCast
round_add_ofNat 📖	mathematical	—	round Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	round_add_natCast
round_add_one 📖	mathematical	—	round Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	round_add_intCast Int.cast_one
round_eq 📖	mathematical	—	round DivisionRing.toRing Field.toDivisionRing Int.floor Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Int.cast_mul_floor_div_cancel_of_pos two_pos Int.instZeroLEOneClass Int.instAddLeftMono round_eq_div Int.cast_ofNat one_div mul_add Distrib.leftDistribClass mul_inv_cancel₀ IsStrictOrderedRing.toCharZero Int.floor_add_one
round_eq_div 📖	mathematical	—	round Int.floor Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Int.floor_add_fract round.eq_1 Int.fract_intCast_add Int.fract_fract Int.floor_intCast_add mul_add Distrib.leftDistribClass Int.cast_ofNat Int.cast_mul Int.ceil_intCast_add add_assoc two_ne_zero Int.floor_eq_zero_iff lt_of_le_of_lt le_mul_of_one_le_left IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero IsStrictOrderedRing.toPosMulStrictMono instNontrivialOfCharZero zero_add Int.cast_one mul_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.Contrapose.contrapose₂ lt_imp_lt_of_le_of_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo le_refl MulZeroClass.mul_zero NeZero.charZero_one Int.instCharZero sub_self LT.lt.le Int.fract_lt_one
round_eq_half_ceil_two_mul 📖	mathematical	—	round Int.ceil Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat em Int.ceil_intCast Int.even_or_odd round_intCast two_mul two_ne_zero mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE ZeroLEOneClass.neZero.two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Int.cast_mul Int.cast_ofNat Int.mul_fract_eq_one_iff_exists_int one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.cast_one Int.cast_one round_eq_div Int.ceil_eq_floor_add_one_iff_notMem
round_eq_iff 📖	mathematical	—	round DivisionRing.toRing Field.toDivisionRing Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddGroupWithOne.toIntCast DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo round_eq Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing add_sub_assoc Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat AddGroup.toOrderedSub
round_eq_zero_iff 📖	mathematical	—	round DivisionRing.toRing Field.toDivisionRing Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Int.cast_zero one_div zero_sub zero_add
round_intCast 📖	mathematical	—	round AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	Int.fract_intCast MulZeroClass.mul_zero IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Int.floor_intCast
round_intCast_add 📖	mathematical	—	round Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	add_comm round_add_intCast
round_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toIntCast round	—	abs_sub_round_eq_min min_le_iff le_or_gt abs_eq_self IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Int.fract_add_floor add_sub_assoc IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Int.le_floor abs_eq_neg_self LT.lt.le sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd add_comm neg_add neg_sub le_add_neg_iff_add_le sub_add_cancel le_sub_comm Nat.cast_one Int.cast_one Int.floor_lt
round_le_add_half 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing round Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat round_eq Int.floor_le
round_natCast 📖	mathematical	—	round AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Int.fract_natCast MulZeroClass.mul_zero IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Int.floor_natCast
round_natCast_add 📖	mathematical	—	round Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	add_comm round_add_natCast
round_neg_two_inv 📖	mathematical	—	round DivisionRing.toRing Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsRat.neg_to_eq Mathlib.Meta.NormNum.isRat_neg Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.isRat_lt_true DivisionRing.toNontrivial
round_ofNat 📖	mathematical	—	round	—	round_natCast
round_ofNat_add 📖	mathematical	—	round Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	round_natCast_add
round_one 📖	mathematical	—	round AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Int.fract_one MulZeroClass.mul_zero IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Int.floor_one
round_sub_intCast 📖	mathematical	—	round SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddGroupWithOne.toIntCast	—	sub_eq_add_neg round_add_intCast
round_sub_natCast 📖	mathematical	—	round SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	Int.cast_natCast round_sub_intCast
round_sub_ofNat 📖	mathematical	—	round SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	round_sub_natCast
round_sub_one 📖	mathematical	—	round SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	round_sub_intCast Int.cast_one
round_two_inv 📖	mathematical	—	round DivisionRing.toRing Field.toDivisionRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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 Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero
round_zero 📖	mathematical	—	round MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Int.fract_zero MulZeroClass.mul_zero IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Int.floor_zero
sub_half_lt_round 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat AddGroupWithOne.toIntCast round	—	Nat.instAtLeastTwoHAddOfNat round_eq Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul 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_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul CancelDenoms.add_subst Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt IsStrictOrderedRing.toIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Int.sub_one_lt_floor

---

← Back to Index