Init

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

Statistics

Metric	Count
Definitions NNRat, cast, den, instNNRatCast, num, NNRatCast, nnratCast, toCoeHTCT, toCoeTail, instNNRatCast, termℚ, «termℚ≥0»	12
Theorems cast_eq_id, cast_id, den_mk, num_mk, cast_eq_id, cast_id	6
Total	18

NNRat

Definitions

Name	Category	Theorems
cast 📖	CompOp	194 math math: Rat.cast_nnratCast, coe_floor, cast_strictMono, Field.nnratCast_def, Finset.card_mul_cast_addConst, not_cast_lt_zero, cast_eq_zero, abs_coe, Polynomial.nnqsmul_eq_C_mul, den_coe, coe_natCast, Rat.coe_nnabs, dist_eq, cast_one, coe_sub, cast_commute, cast_listProd, cast_def, cast_add_of_ne_zero, cast_le, floor_coe, canLift, cast_add, Nonneg.mk_nnratCast, coe_zero, NNRatCast.toOfScientific_def, HahnSeries.single_zero_nnratCast, coe_divNat, cast_mono, coe_max, coe_indicator, Semifield.nnratCast_def, cast_div, Mathlib.Tactic.Qify.nnratCast_le, coe_zpow, cast_inj, coe_mk, floor_cast, coe_pos, Finset.cast_subConst_mul_card, Quaternion.imJ_nnratCast, Real.ofCauchy_nnratCast, cast_multisetProd, coe_injective, one_le_cast, Nonneg.coe_nnratCast, cast_eq_id, AddOpposite.unop_nnratCast, Real.nnnorm_nnratCast, MulOpposite.unop_nnratCast, coe_lt_coe, Complex.im_nnratCast, Complex.norm_nnratCast, coe_eq_zero, intCeil_cast, DivisionSemiring.nnqsmul_def, Quaternion.imI_nnratCast, RCLike.nnnorm_nnratCast, Finset.card_mul_cast_subConst, coe_add, Quaternion.imK_nnratCast, cast_nonneg, cast_prod, coe_castHom, map_nnratCast, preimage_cast_Iic, natCast_le_cast, coe_ceil, preimage_cast_Ioi, Complex.ofReal_nnratCast, natCast_lt_cast, cast_le_one, SubfieldClass.coe_nnratCast, cast_sum, coe_div, ULift.down_nnratCast, Real.cauchy_nnratCast, bddBelow_coe, preimage_cast_uIcc, cast_zpow, preimage_cast_Icc, cast_injective, DivisionSemiring.nnratCast_def, coe_inv, Finset.cast_mulConst_mul_card, cast_pow, coe_le_coe, natAbs_num_coe, cast_ofScientific, cast_multisetSum, preimage_cast_Ici, ceil_coe, Complex.nnnorm_nnratCast, cast_min, one_lt_cast, sub_def, Finset.cast_subConst, star_nnratCast, ENNReal.coe_nnratCast, Finset.nnratCast_dens, cast_max, CauSeq.Completion.ofRat_nnratCast, DivisionRing.nnqsmul_def, Quaternion.im_nnratCast, Finset.cast_mulConst, cast_pos, cast_zpow_of_ne_zero, Mathlib.Tactic.Qify.nnratCast_lt, nsmul_coe, Finset.card_mul_cast_mulConst, ofNat_le_cast, cast_mul, Semifield.nnqsmul_def, ceil_cast, cast_smul_eq_nnqsmul, Quaternion.coe_nnratCast, Mathlib.Tactic.Qify.nnratCast_eq, RCLike.norm_nnratCast, ext_iff, AddOpposite.op_nnratCast, coe_mono, RCLike.ofReal_nnratCast, val_eq_cast, preimage_cast_Ico, coe_nonneg, cast_nonpos, toNNRat_coe, Finset.natCast_card_mul_nnratCast_dens, coe_one, Finset.cast_addConst_mul_card, Rat.le_toNNRat_iff_coe_le', nndist_eq, cast_inv, cast_div_of_ne_zero, Rat.le_toNNRat_iff_coe_le, smul_one_eq_cast, Rat.toNNRat_le_iff_le_coe, Finset.cast_divConst_mul_card, cast_ofNat, selfAdjoint.val_nnratCast, cast_divNat_of_ne_zero, preimage_cast_Ioo, Rat.toNNRat_lt_iff_lt_coe, coe_mul, Finset.cast_divConst, cast_lt_one, map_nnratCast_smul, eq_nnratCast, preimage_cast_Ioc, cast_comm, cast_lt, IsSelfAdjoint.nnratCast, cast_zero, Rat.lt_toNNRat_iff_coe_lt, ULift.up_nnratCast, SubfieldClass.nnratCast_mem, commute_cast, cast_le_natCast, DivisionRing.nnratCast_def, Rat.le_coe_toNNRat, cast_id, DirectLimit.nnratCast_def, cast_mk, cast_divNat, coe_pow, bddAbove_coe, cast_lt_natCast, cast_natCast, Field.nnqsmul_def, cast_inv_of_ne_zero, coe_inj, coe_min, intFloor_cast, MulOpposite.op_nnratCast, smul_def, nnratCast_smul_eq, cast_le_ofNat, Finset.nnratCast_dens_mul_natCast_card, cast_lt_ofNat, Real.norm_nnratCast, Finset.card_mul_cast_divConst, Complex.re_nnratCast, Finset.cast_addConst, preimage_cast_Iio, ofNat_lt_cast, cast_mul_of_ne_zero, Rat.coe_toNNRat, castOrderEmbedding_apply, Quaternion.re_nnratCast, num_coe, preimage_cast_uIoc, cast_lt_zero, cast_listSum, coe_coeHom
den 📖	CompOp	33 math math: Field.nnratCast_def, le_def, den_coe, mul_def, den_natCast, num_inv_of_ne_zero, cast_def, lt_def, Semifield.nnratCast_def, mul_den_eq_num, den_mul_den_eq_den_mul_gcd, den_ofNat, ext_num_den_iff, add_def, num_mul_num_eq_num_mul_gcd, div_def, mul_den, DivisionSemiring.nnratCast_def, den_pow, coprime_num_den, inv_def, den_pos, den_inv_of_ne_zero, num_divNat_den, floor_def, den_zero, DivisionRing.nnratCast_def, mul_num, den_mk, den_mul_eq_num, DivisibleHull.nnqsmul_mk, den_one, num_div_den
instNNRatCast 📖	CompOp	3 math math: cast_eq_id, cast_ofScientific, cast_id
num 📖	CompOp	35 math math: Field.nnratCast_def, num_pow, le_def, mul_def, num_inv_of_ne_zero, cast_def, lt_def, Semifield.nnratCast_def, num_pos, mul_den_eq_num, Mathlib.Meta.Positivity.NNRat.num_pos_of_pos, den_mul_den_eq_den_mul_gcd, ext_num_den_iff, add_def, num_one, num_mul_num_eq_num_mul_gcd, num_zero, div_def, mul_den, num_ofNat, DivisionSemiring.nnratCast_def, num_natCast, natAbs_num_coe, coprime_num_den, inv_def, num_mk, den_inv_of_ne_zero, num_divNat_den, floor_def, DivisionRing.nnratCast_def, mul_num, den_mul_eq_num, DivisibleHull.nnqsmul_mk, num_coe, num_div_den

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_eq_id 📖	mathematical	—	cast NNRat instNNRatCast	—	—
cast_id 📖	mathematical	—	cast NNRat instNNRatCast	—	—
den_mk 📖	mathematical	—	den	—	—
num_mk 📖	mathematical	—	num	—	—

NNRatCast

Definitions

Name	Category	Theorems
nnratCast 📖	CompOp	—
toCoeHTCT 📖	CompOp	—
toCoeTail 📖	CompOp	—

Rat

Definitions

Name	Category	Theorems
instNNRatCast 📖	CompOp	56 math math: cast_nnratCast, NNRat.coe_floor, NNRat.abs_coe, NNRat.den_coe, NNRat.coe_natCast, coe_nnabs, NNRat.dist_eq, NNRat.coe_sub, NNRat.floor_coe, NNRat.canLift, NNRat.coe_zero, NNRat.coe_divNat, NNRat.coe_max, NNRat.coe_indicator, Mathlib.Tactic.Qify.nnratCast_le, NNRat.coe_zpow, NNRat.coe_mk, NNRat.coe_pos, NNRat.coe_injective, NNRat.coe_lt_coe, NNRat.coe_eq_zero, NNRat.intCeil_cast, NNRat.coe_add, NNRat.coe_ceil, NNRat.coe_div, NNRat.bddBelow_coe, NNRat.coe_inv, NNRat.coe_le_coe, NNRat.natAbs_num_coe, NNRat.ceil_coe, NNRat.sub_def, Mathlib.Tactic.Qify.nnratCast_lt, NNRat.nsmul_coe, Mathlib.Tactic.Qify.nnratCast_eq, NNRat.ext_iff, NNRat.coe_mono, NNRat.val_eq_cast, NNRat.coe_nonneg, NNRat.toNNRat_coe, NNRat.coe_one, le_toNNRat_iff_coe_le', NNRat.nndist_eq, le_toNNRat_iff_coe_le, toNNRat_le_iff_le_coe, toNNRat_lt_iff_lt_coe, NNRat.coe_mul, lt_toNNRat_iff_coe_lt, le_coe_toNNRat, NNRat.coe_pow, NNRat.bddAbove_coe, NNRat.coe_inj, NNRat.coe_min, NNRat.intFloor_cast, coe_toNNRat, NNRat.num_coe, NNRat.coe_coeHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_eq_id 📖	—	—	—	—	—
cast_id 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
NNRat 📖	CompOp	340 math math: Finset.expect_ite_mem, Finset.dens_union_of_disjoint, NNRat.coe_floor, NNRat.cast_strictMono, StarAddMonoid.toStarModuleNNRat, AddDissociated.randomisation, NNRat.num_pow, Finset.dens_cons, NNRat.le_def, NNRat.cast_eq_zero, Finset.dens_map_le, Rat.toNNRat_mul, Polynomial.nnqsmul_eq_C_mul, Finset.addConst_le_inv_dens, RCLike.norm_expect_le, Finset.dens_inter_add_dens_sdiff, Finset.mulConst_mul_card, Finset.card_mul_divConst, Finset.card_mul_dens, NNRat.coe_natCast, NNRat.mul_def, Finset.card_mul_subConst, Complex.re_balance, Fintype.expect_dite_eq, NNRat.den_natCast, NNRat.dist_eq, NNRat.cast_one, Finset.one_le_mulConst_self, NNRat.cast_listProd, NNRat.num_inv_of_ne_zero, NNRat.instStarOrderedRing, Complex.im_expect, NNRat.cast_add_of_ne_zero, NNRat.instSMulCommClass', NNRat.cast_le, NNRat.floor_coe, NNRat.canLift, Finset.subConst_le_addConst_sq, Finset.dens_sdiff_add_dens_inter, RCLike.ofReal_balance, NNRat.cast_add, Ring.choose_eq_smul, NNRat.coe_zero, NNRat.lt_def, Finset.divConst_mul_card, Fintype.expect_ite_eq, MvPolynomial.schwartz_zippel_totalDegree, RCLike.ofReal_comp_balance, Finset.mulConst_le_card, NNRat.toNNRat_sum_of_nonneg, Fintype.expect_ite_zero, NNRat.cast_mono, Finset.dens_union_add_dens_inter, Finset.expect_ite_zero, Complex.im_nnqsmul, Finset.dens_eq_sum_dens_image, NNRat.coe_max, Finset.card_mul_addConst, RCLike.wInner_cWeight_eq_expect, SubfieldClass.nnqsmul_mem, NNRat.coe_indicator, Fintype.expect_dite_eq', NNRat.cast_div, NNRat.num_pos, Mathlib.Tactic.Qify.nnratCast_le, NNRat.coe_zpow, Finset.divConst_le_card, Finset.one_le_mulConst, NNRat.mul_den_eq_num, abs_nnqsmul, NNRat.floor_cast, NNRat.coe_pos, Finset.divConst_le_mulConst_sq, NNRat.toNNRat_coe_nat, NNRat.cast_multisetProd, Finset.pluennecke_ruzsa_inequality_nsmul_add, instIsStrictOrderedRingNNRat, NNRat.coe_injective, NNRat.den_mul_den_eq_den_mul_gcd, Rat.toNNRat_lt_toNNRat_iff', NNRat.one_le_cast, PosSMulMono.nnrat_of_rat, Complex.re_comp_balance, NNRat.cast_eq_id, NNRat.add_def, NNRat.instContinuousSub, map_nnrat_smul, Finset.dens_le_one, Rat.toNNRat_div', AddChar.expect_apply_eq_zero_iff_ne_zero, Complex.ofReal_balance, instMulArchimedeanNNRat, NNRat.coe_lt_coe, NNRat.coe_eq_zero, Finset.card_mul_mulConst, Finset.addConst_le_subConst_sq, NNRat.isFractionRing, NNRat.coe_add, Finset.expect_eq_single_of_mem, NNRat.cast_prod, NNRat.coe_castHom, NNRat.mk_natCast, DivisibleHull.instIsStrictOrderedModuleNNRat, Finset.dens_eq_card_div_card, Finset.dens_disjiUnion, NNRat.nonpos_iff_eq_zero, star_nnrat_smul, Rat.toNNRat_lt_toNNRat_iff_of_nonneg, NNRat.preimage_cast_Iic, NNRat.natCast_le_cast, NNRat.instContinuousInv₀, binomialSeries_apply, NNRat.num_one, NNRat.coe_ceil, NNRat.preimage_cast_Ioi, Finset.nonneg_addConst, Finset.mulConst_empty_left, Rat.toNNRat_div, Finset.dens_strictMono, Finset.dens_eq_one, SubfieldClass.coe_nnqsmul, NNRat.num_mul_num_eq_num_mul_gcd, Finset.dens_sdiff_add_dens, NNRat.instCharZero, NNRat.natCast_lt_cast, NNRat.tendsto_inv_atTop_nhds_zero_nat, NNRat.cast_le_one, NNRat.cast_sum, NNRat.coe_div, NNRat.instContinuousSMulOfIsScalarTowerOfRat, Finset.pluennecke_ruzsa_inequality_pow_div_pow_mul, NNRat.num_zero, Finset.addConst_le_card, Finset.dens_mul_card, NNRat.div_def, Finset.expect_boole_mul', NNRat.bddBelow_coe, NNRat.mul_den, Finset.one_le_divConst, NNRat.preimage_cast_uIcc, NNRat.cast_zpow, NNRat.preimage_cast_Icc, Finset.dens_empty, NNRat.cast_injective, NNRat.coe_inv, NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat, Finset.dens_biUnion_le, instArchimedeanNNRat, Finset.expect_dite_eq', RCLike.wInner_cWeight_const_left, Finset.dens_le_dens_sdiff_add_dens, Finset.dens_lt_dens, NNRat.num_natCast, AddChar.expect_eq_zero_iff_ne_zero, NNRat.cast_pow, Complex.ofReal_comp_balance, Nonneg.coe_nnqsmul, Finset.nonneg_addConst_self, NNRat.den_pow, MvPolynomial.schwartz_zippel_sup_sum, NNReal.coe_nnqsmul, Rat.toNNRat_of_nonpos, NNRat.instCanonicallyOrderedAdd, Finset.divConst_empty_left, NNRat.coe_le_coe, Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero, Complex.im_balance, Complex.ofReal_expect, Fintype.expect_ite_mem, Finset.pluennecke_ruzsa_inequality_pow_div, DivisibleHull.qsmul_def, Finset.mulConst_le_inv_dens, Rat.toNNRat_pos, NNRat.addSubmonoid_closure_range_pow, NNRat.cast_ofScientific, NNRat.cast_multisetSum, Finset.addConst_mul_card, NNRat.preimage_cast_Ici, star_nnqsmul, NNRat.ceil_coe, Finset.le_dens_sdiff, NNRat.instSMulCommClass, Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub, NNRat.inv_def, NNRat.cast_min, Finset.expect_boole_mul, DivisibleHull.qsmul_of_nonneg, NNRat.toNNRat_mono, Complex.im_comp_balance, PosSMulStrictMono.nnrat_of_rat, NNRat.one_lt_cast, Rat.toNNRat_add_le, NNRat.sub_def, NNRat.instTrivialStar, NNReal.coe_expect, NNRat.divNat_zero, Finset.subConst_le_card, NNRat.cast_max, subsingleton_nnrat_module, RCLike.ofReal_expect, Finset.dens_filter_add_dens_filter_not_eq_dens, LinearOrderedSemifield.toPosSMulStrictMono_rat, Finset.dens_mono, NNRat.instOrderedSub, NNRat.cast_pos, NNRat.divNat_mul_divNat, NNRat.cast_zpow_of_ne_zero, Mathlib.Tactic.Qify.nnratCast_lt, Finset.subConst_mul_card, NNRat.nsmul_coe, Finset.dens_inter_add_dens_union, NNRat.ofNat_le_cast, NNRat.cast_mul, NNRat.ceil_cast, Finset.dens_singleton, Nonneg.mk_nnqsmul, NNRat.cast_smul_eq_nnqsmul, Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero, NNRat.toNNRat_prod_of_nonneg, Finset.nonneg_subConst_self, NNRat.coe_mono, NNRat.preimage_cast_Ico, Rat.toNNRat_add, NNRat.cast_nonpos, Rat.toNNRat_inv, NNRat.coe_one, Finset.expect_univ, Finset.one_le_divConst_self, NNRat.nndist_eq, RingHomClass.toLinearMapClassNNRat, NNRat.cast_inv, NNRat.instContinuousSMulNNReal, NNRat.cast_div_of_ne_zero, Finset.subConst_empty_right, Rat.toNNRat_le_toNNRat_iff, Rat.le_toNNRat_iff_coe_le, NNRat.smul_one_eq_cast, Rat.toNNRat_le_iff_le_coe, NNRat.instOrderTopology, Finset.mulConst_empty_right, Finset.dens_biUnion, Finset.addConst_empty_left, Finset.dens_eq_zero, Finset.dens_sdiff_add_dens_eq_dens, Finset.dens_disjUnion, Finset.subConst_le_inv_dens, RCLike.nnnorm_nnqsmul, NNRat.den_inv_of_ne_zero, DivisibleHull.qsmul_of_nonpos, Rat.toNNRat_one, NNRat.preimage_cast_Ioo, Finset.addConst_empty_right, Rat.toNNRat_lt_iff_lt_coe, Finset.expect_dite_eq, NNRat.coe_mul, NNRat.cast_lt_one, eq_nnratCast, NNRat.floor_def, NNRat.instIsScalarTowerRight, NNRat.preimage_cast_Ioc, Finset.pluennecke_ruzsa_inequality_pow_div_pow_div, Finset.expect_apply, NNRat.cast_lt, NNRat.den_zero, Complex.re_expect, NNRat.cast_zero, Rat.lt_toNNRat_iff_coe_lt, Complex.re_nnqsmul, Rat.toNNRat_zero, MvPolynomial.schwartz_zippel_sum_degreeOf, RCLike.wInner_cWeight_const_right, Finset.expect_div, NNRat.cast_le_natCast, MeasureTheory.lpNorm_expect_le, Fintype.expect_ite_eq', Finset.pluennecke_ruzsa_inequality_pow_mul, Finset.dens_sdiff, NNRat.addSubmonoid_closure_range_mul_self, NNRat.cast_id, NNRat.mul_num, Finset.pluennecke_ruzsa_inequality_nsmul_sub, Finset.dens_eq_sum_dens_fiberwise, Rat.toNNRat_eq_zero, NNRat.floor_natCast_div_natCast, SMulCommClass.nnrat, NNRat.instIsTopologicalSemiring, NNRat.coe_pow, NNRat.bddAbove_coe, Real.compact_inner_le_weight_mul_Lp_of_nonneg, NNRat.cast_lt_natCast, Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add, NNRat.cast_natCast, algebraMap.coe_expect, Finset.subConst_empty_left, Rat.toNNRat_lt_toNNRat_iff, Complex.ofReal_nnqsmul, NNRat.cast_inv_of_ne_zero, Numbering.dens_prefixed, NNRat.coe_min, Finset.dens_union_le, Finset.expect_eq_sum_div_card, AddChar.expect_apply_eq_ite, NNRat.smul_def, Finset.expect_ite_eq, Finset.divConst_empty_right, Finset.Nonempty.dens_pos, SMulCommClass.nnrat', NNRat.cast_le_ofNat, IsScalarTower.nnrat, NNRat.den_mul_eq_num, Finset.dens_le_dens, NNRat.instNontrivial, Finset.divConst_le_inv_dens, MonoidWithZeroHomClass.ext_nnrat_iff, NNRat.cast_lt_ofNat, Finset.expect_ite_eq', Finset.dens_univ, Finset.mulConst_le_divConst_sq, NNRat.preimage_cast_Iio, RCLike.wInner_cWeight_eq_smul_wInner_one, NNRat.ofNat_lt_cast, DivisibleHull.nnqsmul_mk, NNRat.den_one, AddChar.expect_eq_ite, NNRat.cast_mul_of_ne_zero, Complex.ofReal_choose, nnqsmul_nonneg, NNRat.castOrderEmbedding_apply, selfAdjoint.val_nnqsmul, NNRat.natCast_eq_divNat, NNRat.preimage_cast_uIoc, NNRat.subsingleton_ringHom, NNRat.num_div_den, Finset.dens_pos, Finset.nonneg_subConst, NNRat.cast_lt_zero, RCLike.norm_nnqsmul, NNRat.cast_listSum, Fintype.expect_eq_sum_div_card, NNRat.coe_coeHom
NNRatCast 📖	CompData	—
termℚ 📖	CompOp	—
«termℚ≥0» 📖	CompOp	—

---

← Back to Index