Rat

📁 Source: Mathlib/Algebra/Field/Rat.lean

Statistics

Metric	Count
Definitions instDiv, instInv, instSemifield, instZPow, instDivisionRing, instField	6
Theorems coe_div, coe_inv, coe_zpow, den_inv_of_ne_zero, div_def, inv_def, num_div_den, num_inv_of_ne_zero, div_nonneg, inv_nonneg	10
Total	16

NNRat

Definitions

Name	Category	Theorems
instDiv 📖	CompOp	21 math math: Finset.expect_ite_mem, MvPolynomial.schwartz_zippel_totalDegree, cast_div, Finset.pluennecke_ruzsa_inequality_nsmul_add, Rat.toNNRat_div', Finset.dens_eq_card_div_card, Rat.toNNRat_div, coe_div, Finset.pluennecke_ruzsa_inequality_pow_div_pow_mul, div_def, MvPolynomial.schwartz_zippel_sup_sum, Finset.pluennecke_ruzsa_inequality_pow_div, Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub, cast_div_of_ne_zero, Finset.pluennecke_ruzsa_inequality_pow_div_pow_div, MvPolynomial.schwartz_zippel_sum_degreeOf, Finset.pluennecke_ruzsa_inequality_pow_mul, Finset.pluennecke_ruzsa_inequality_nsmul_sub, floor_natCast_div_natCast, Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add, num_div_den
instInv 📖	CompOp	30 math math: Finset.dens_cons, Finset.addConst_le_inv_dens, Fintype.expect_dite_eq, num_inv_of_ne_zero, Fintype.expect_ite_eq, Fintype.expect_ite_zero, Finset.expect_ite_zero, Fintype.expect_dite_eq', Finset.expect_eq_single_of_mem, instContinuousInv₀, tendsto_inv_atTop_nhds_zero_nat, coe_inv, tendsto_algebraMap_inv_atTop_nhds_zero_nat, Finset.expect_dite_eq', Finset.mulConst_le_inv_dens, inv_def, Finset.dens_singleton, Rat.toNNRat_inv, Finset.expect_univ, cast_inv, Finset.subConst_le_inv_dens, den_inv_of_ne_zero, Finset.expect_dite_eq, Fintype.expect_ite_eq', cast_inv_of_ne_zero, Numbering.dens_prefixed, Finset.expect_ite_eq, Finset.divConst_le_inv_dens, Finset.expect_ite_eq', RCLike.wInner_cWeight_eq_smul_wInner_one
instSemifield 📖	CompOp	162 math math: Finset.expect_ite_mem, Finset.dens_union_of_disjoint, coe_floor, StarAddMonoid.toStarModuleNNRat, Finset.dens_cons, cast_eq_zero, Finset.dens_inter_add_dens_sdiff, Finset.mulConst_mul_card, Finset.card_mul_divConst, Finset.card_mul_dens, Finset.card_mul_subConst, Fintype.expect_dite_eq, cast_one, Finset.one_le_mulConst_self, cast_listProd, cast_add_of_ne_zero, floor_coe, Finset.subConst_le_addConst_sq, Finset.dens_sdiff_add_dens_inter, cast_add, Finset.divConst_mul_card, Fintype.expect_ite_eq, MvPolynomial.schwartz_zippel_totalDegree, Finset.mulConst_le_card, toNNRat_sum_of_nonneg, Fintype.expect_ite_zero, Finset.dens_union_add_dens_inter, Finset.expect_ite_zero, Finset.dens_eq_sum_dens_image, Finset.card_mul_addConst, coe_indicator, Fintype.expect_dite_eq', Finset.divConst_le_card, Finset.one_le_mulConst, abs_nnqsmul, floor_cast, Finset.divConst_le_mulConst_sq, Finset.pluennecke_ruzsa_inequality_nsmul_add, den_mul_den_eq_den_mul_gcd, one_le_cast, PosSMulMono.nnrat_of_rat, map_nnrat_smul, Finset.dens_le_one, Finset.card_mul_mulConst, Finset.addConst_le_subConst_sq, Finset.expect_eq_single_of_mem, coe_castHom, DivisibleHull.instIsStrictOrderedModuleNNRat, Finset.dens_eq_card_div_card, Finset.dens_disjiUnion, star_nnrat_smul, natCast_le_cast, instContinuousInv₀, coe_ceil, Finset.nonneg_addConst, Finset.mulConst_empty_left, Finset.dens_eq_one, num_mul_num_eq_num_mul_gcd, Finset.dens_sdiff_add_dens, natCast_lt_cast, tendsto_inv_atTop_nhds_zero_nat, cast_le_one, cast_sum, instContinuousSMulOfIsScalarTowerOfRat, Finset.pluennecke_ruzsa_inequality_pow_div_pow_mul, Finset.addConst_le_card, Finset.dens_mul_card, mul_den, Finset.one_le_divConst, Finset.dens_empty, tendsto_algebraMap_inv_atTop_nhds_zero_nat, Finset.dens_biUnion_le, instArchimedeanNNRat, Finset.expect_dite_eq', Finset.dens_le_dens_sdiff_add_dens, cast_pow, Finset.nonneg_addConst_self, MvPolynomial.schwartz_zippel_sup_sum, Finset.divConst_empty_left, Fintype.expect_ite_mem, Finset.pluennecke_ruzsa_inequality_pow_div, DivisibleHull.qsmul_def, addSubmonoid_closure_range_pow, cast_multisetSum, Finset.addConst_mul_card, star_nnqsmul, ceil_coe, Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub, DivisibleHull.qsmul_of_nonneg, PosSMulStrictMono.nnrat_of_rat, one_lt_cast, instTrivialStar, Finset.subConst_le_card, subsingleton_nnrat_module, Finset.dens_filter_add_dens_filter_not_eq_dens, LinearOrderedSemifield.toPosSMulStrictMono_rat, cast_pos, Finset.subConst_mul_card, Finset.dens_inter_add_dens_union, ofNat_le_cast, cast_mul, ceil_cast, Finset.dens_singleton, cast_smul_eq_nnqsmul, Finset.nonneg_subConst_self, cast_nonpos, Finset.expect_univ, Finset.one_le_divConst_self, RingHomClass.toLinearMapClassNNRat, Finset.subConst_empty_right, 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, DivisibleHull.qsmul_of_nonpos, Finset.addConst_empty_right, Finset.expect_dite_eq, cast_lt_one, floor_def, Finset.pluennecke_ruzsa_inequality_pow_div_pow_div, Finset.expect_apply, cast_zero, MvPolynomial.schwartz_zippel_sum_degreeOf, cast_le_natCast, MeasureTheory.lpNorm_expect_le, Fintype.expect_ite_eq', Finset.pluennecke_ruzsa_inequality_pow_mul, addSubmonoid_closure_range_mul_self, mul_num, Finset.pluennecke_ruzsa_inequality_nsmul_sub, Finset.dens_eq_sum_dens_fiberwise, floor_natCast_div_natCast, SMulCommClass.nnrat, instIsTopologicalSemiring, cast_lt_natCast, Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add, cast_natCast, Finset.subConst_empty_left, Numbering.dens_prefixed, Finset.dens_union_le, Finset.expect_ite_eq, Finset.divConst_empty_right, Finset.Nonempty.dens_pos, SMulCommClass.nnrat', cast_le_ofNat, IsScalarTower.nnrat, MonoidWithZeroHomClass.ext_nnrat_iff, cast_lt_ofNat, Finset.expect_ite_eq', Finset.dens_univ, Finset.mulConst_le_divConst_sq, RCLike.wInner_cWeight_eq_smul_wInner_one, ofNat_lt_cast, DivisibleHull.nnqsmul_mk, cast_mul_of_ne_zero, subsingleton_ringHom, Finset.dens_pos, Finset.nonneg_subConst, cast_lt_zero, cast_listSum
instZPow 📖	CompOp	3 math math: coe_zpow, cast_zpow, cast_zpow_of_ne_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_div 📖	mathematical	—	cast Rat.instNNRatCast NNRat instDiv	—	—
coe_inv 📖	mathematical	—	cast Rat.instNNRatCast NNRat instInv	—	—
coe_zpow 📖	mathematical	—	cast Rat.instNNRatCast NNRat instZPow	—	—
den_inv_of_ne_zero 📖	mathematical	—	den NNRat instInv num	—	inv_def divNat.eq_1 den.eq_1 num_ne_zero coprime_num_den
div_def 📖	mathematical	—	NNRat instDiv divNat num den	—	ext Rat.div_def' num_coe Nat.cast_mul
inv_def 📖	mathematical	—	NNRat instInv divNat den num	—	ext num_coe
num_div_den 📖	mathematical	—	NNRat instDiv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringNNRat num den	—	ext coe_div coe_natCast num.eq_1 Int.cast_natCast cast_def
num_inv_of_ne_zero 📖	mathematical	—	num NNRat instInv den	—	inv_def divNat.eq_1 num.eq_1 num_ne_zero coprime_num_den

Rat

Definitions

Name	Category	Theorems
instDivisionRing 📖	CompOp	113 math math: num_lt_succ_floor_mul_den, NNRat.coe_floor, GenContFract.IntFractPair.coe_stream_nth_rat_eq, GenContFract.coe_of_h_rat_eq, Real.ofCauchy_sup, GenContFract.coe_of_s_rat_eq, cast_fract, ceil_intCast_div_natCast, NNRat.floor_coe, isFractionRingDen, GenContFract.of_terminates_iff_of_rat_terminates, Real.ofCauchy_zero, instSubsingletonSubfieldRat, Real.of_near, CongruenceSubgroup.exists_Gamma_le_conj, Real.ofCauchy_mul, GenContFract.IntFractPair.coe_stream'_rat_eq, Real.cauchy_sub, Real.mk_one, associated_num_den, GenContFract.IntFractPair.exists_nth_stream_eq_none_of_rat, floor_natCast_div_natCast, Real.ofCauchy_nnratCast, castHom_rat, Real.lt_cauchy, round_cast, CauSeq.Completion.ofRat_rat, cast_list_prod, Real.ofCauchy_sub, Real.mk_lt, NNRat.intCeil_cast, floor_cast, GenContFract.IntFractPair.coe_of_rat_eq, GenContFract.coe_of_rat_eq, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, NNRat.coe_ceil, Nat.Ioc_filter_modEq_card, ceil_natCast_div_natCast, Int.Ioc_filter_modEq_card, Real.mk_mul, Real.cauchy_inv, Real.cauchy_nnratCast, NumberField.to_finiteDimensional, GenContFract.IntFractPair.of_inv_fr_num_lt_num_of_pos, Real.mk_add, Nat.Ico_filter_modEq_card, natFloor_natCast_div_natCast, Polynomial.bernoulli_eq_sub_sum, NumberField.integralBasis_repr_apply, GaussianInt.div_def, Int.Ico_filter_dvd_card, GenContFract.coe_of_s_get?_rat_eq, Real.ofCauchy_natCast, fract_inv_num_lt_num_of_pos, den_le_and_le_num_le_of_sub_lt_one_div_den_sq, Real.cauchy_natCast, Subfield.bot_eq_of_charZero, isFractionRing, Real.ofCauchy_ratCast, Nat.coprime_sub_mul_floor_rat_div_of_coprime, NNRat.ceil_coe, NumberField.finite_of_discr_bdd, Real.ofCauchy_intCast, isFractionRingNum, Real.ofCauchy_div, isLocalizationIsInteger_iff, floor_def', Real.cauchy_neg, uniformSpace_eq, Real.mk_const, ringOfIntegersEquiv_apply_coe, Real.cauchy_intCast, Real.mk_zero, Real.cauchy_add, Real.ofCauchy_add, Real.ofCauchy_inv, Real.cauchy_zero, Matrix.num_one, Real.ofCauchy_neg, Int.Ico_filter_modEq_card, Int.Ioc_filter_dvd_eq, Real.mk_inf, ceil_cast, Real.mk_eq, Real.ofCauchy_one, FractionalIdeal.abs_det_basis_change, Real.mk_sup, Polynomial.bernoulli_one, Real.cauchy_one, GenContFract.terminates_of_rat, instIsLocalizationIntPosRat, Real.cauchy_ratCast, Nat.count_modEq_card_eq_ceil, Matrix.den_one, Real.cauchy_mul, Real.ringEquivCauchy_apply, Real.mk_neg, instNonemptySeedRatReal, Polynomial.bernoulli_comp_one_sub_X, NNRat.intFloor_cast, den_intFract, Polynomial.bernoulli_comp_neg_X, Int.mod_nat_eq_sub_mul_floor_rat_div, Int.Ico_filter_dvd_eq, Real.mk_le, Real.ringEquivCauchy_symm_apply_cauchy, floor_intCast_div_natCast, Real.isCauSeq_iff_lift, ringOfIntegersWithValEquiv_apply, Int.Ioc_filter_dvd_card, ceil_def', Real.ofCauchy_inf, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal
instField 📖	CompOp	138 math math: RingOfIntegers.isUnit_iff, AdjoinRoot.instNumberFieldRat, Polynomial.Gal.galActionHom_bijective_of_prime_degree', PadicInt.isCauSeq_nthHom, NumberField.IsCMField.unitsComplexConj_torsion, Padic.withValUniformEquiv_norm_le_one_iff, Real.ofCauchy_sup, Padic.complete', HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, PadicSeq.ne_zero_iff_nequiv_zero, isFractionRingDen, IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two, Padic.exi_rat_seq_conv_cauchy, Real.ofCauchy_zero, NumberField.discr_rat, Real.of_near, NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic, Real.ofCauchy_mul, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv, IsCyclotomicExtension.Rat.discr_prime_pow', Real.cauchy_sub, Padic.zero_def, Real.mk_one, IsCyclotomicExtension.Rat.absdiscr_prime_pow, associated_num_den, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow, isReal_infinitePlace, Real.ofCauchy_nnratCast, HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, Real.lt_cauchy, IntermediateField.isTotallyReal_bot, padicNormE.defn, CauSeq.Completion.ofRat_rat, Real.ofCauchy_sub, Real.mk_lt, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, valuation_le_one_iff_den, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure, IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, PadicSeq.norm_neg, IsCyclotomicExtension.Rat.discr, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, Real.mk_mul, PadicSeq.norm_nonarchimedean, Real.cauchy_inv, PadicSeq.not_equiv_zero_const_of_nonzero, Real.cauchy_nnratCast, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', Real.mk_add, IsCyclotomicExtension.Rat.absdiscr_prime_pow_succ, PadicInt.coe_adicCompletionIntegersEquiv_apply, NumberField.is_primitive_element_of_infinitePlace_lt, IsCyclotomicExtension.Rat.discr_prime_pow_succ, Real.ofCauchy_natCast, PadicInt.nthHomSeq_mul, Padic.mk_eq, Real.cauchy_natCast, Padic.complete'', IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, Real.ofCauchy_ratCast, numberField, xInTermsOfW_vars_subset, IsCyclotomicExtension.Rat.natAbs_discr, NormedSpace.expSeries_sum_eq_rat, NumberField.finite_of_discr_bdd, Padic.exi_rat_seq_conv, Real.ofCauchy_intCast, NormedSpace.exp_def, PadicSeq.not_limZero_const_of_nonzero, isFractionRingNum, NumberField.IsCMField.unitsMulComplexConjInv_apply, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, IsCyclotomicExtension.Rat.absdiscr_prime, Real.ofCauchy_div, HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, IsCyclotomicExtension.Rat.discr_prime_pow, Real.cauchy_neg, uniformSpace_eq, Real.mk_const, ringOfIntegersEquiv_apply_coe, Real.cauchy_intCast, Real.mk_zero, Real.cauchy_add, Real.ofCauchy_add, cosetToCuspOrbit_apply_mk, Real.ofCauchy_inv, Real.cauchy_zero, Real.ofCauchy_neg, Polynomial.Gal.galActionHom_bijective_of_prime_degree, IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero, Padic.isUniformInducing_cast_withVal, infinitePlace_apply, Real.mk_inf, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime, PadicSeq.add_eq_max_of_ne, NormedSpace.expSeries_eq_expSeries_rat, Real.mk_eq, Real.ofCauchy_one, NumberField.isUnit_iff_norm, PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub, Padic.coe_withValRingEquiv_symm, Real.mk_sup, xInTermsOfW_vars_aux, PadicInt.nthHomSeq_add, ringOfIntegersEquiv_symm_apply_coe, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, HeightOneSpectrum.valuation_equiv_padicValuation, Real.cauchy_one, NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv, PadicInt.nthHomSeq_one, Real.cauchy_ratCast, PadicSeq.norm_const, PadicSeq.norm_one, Real.cauchy_mul, IsCyclotomicExtension.Rat.discr_odd_prime', Real.ringEquivCauchy_apply, PadicSeq.norm_zero_iff, Real.mk_neg, IsCyclotomicExtension.Rat.discr_prime, numberField_discr, NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion, instSubsingletonInfinitePlace, PadicSeq.norm_mul, Padic.const_equiv, NumberField.IsCMField.complexConj_torsion, Real.mk_le, Real.ringEquivCauchy_symm_apply_cauchy, classNumber_eq, Real.isCauSeq_iff_lift, Padic.isDenseInducing_cast_withVal, Real.mk_pos, NumberField.instIsTotallyRealRat, ringOfIntegersWithValEquiv_apply, PadicSeq.eq_zero_iff_equiv_zero, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', Real.ofCauchy_inf, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
div_nonneg 📖	—	—	—	—	mul_nonneg instPosMulMono inv_nonneg
inv_nonneg 📖	—	—	—	—	—

---

← Back to Index