Rat

📁 Source: Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

Statistics

Metric	Count
Definitions `toOfScientific`, `instDistribLattice`, `instInf`, `instLattice`, `instPartialOrder`, `instPreorder`, `instSemilatticeInf`, `instSemilatticeSup`, `instSup`, `linearOrder`	10
Theorems `cast_ofScientific`, `toOfScientific_def`, `abs_def`, `abs_def'`, `den_abs_eq_den`, `divInt_le_divInt`, `div_lt_div_iff_mul_lt_mul`, `instAddLeftMono`, `lt_iff_le_not_ge`, `lt_one_iff_num_lt_denom`, `mkRat_neg`, `mkRat_neg_iff`, `mkRat_nonneg`, `mkRat_nonneg_iff`, `mkRat_nonpos`, `mkRat_nonpos_iff`, `mkRat_pos`, `mkRat_pos_iff`, `num_abs_eq_abs_num`, `num_neg`, `num_nonpos`, `num_pos`, `ofScientific_nonneg`	23
Total	33

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_ofScientific` 📖	mathematical	—	`cast` `NNRat` `NNRatCast.toOfScientific` `instNNRatCast`	—	—

NNRatCast

Definitions

Name	Category	Theorems
`toOfScientific` 📖	CompOp	25 math math: `HahnSeries.single_zero_ofScientific`, `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true`, `toOfScientific_def`, `Real.pi_lt_d6`, `Real.exp_one_gt_d9`, `Real.log_two_gt_d9`, `instLawfulOfScientificOfCharZero`, `Real.pi_gt_d2`, `Behrend.ceil_lt_mul`, `NNReal.coe_ofScientific`, `NNRat.cast_ofScientific`, `Real.pi_lt_d2`, `Real.pi_gt_d4`, `Real.exp_one_lt_d9`, `Real.pi_lt_d20`, `Real.log_two_lt_d9`, `Rat.cast_ofScientific`, `SubfieldClass.ofScientific_mem`, `Real.pi_gt_d20`, `NNRat.Nonneg.coe_ofScientific`, `Real.exp_neg_one_gt_d9`, `Mathlib.Meta.NormNum.isNat_ofScientific_of_false`, `Real.pi_gt_d6`, `Real.exp_neg_one_lt_d9`, `Real.pi_lt_d4`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toOfScientific_def` 📖	mathematical	—	`toOfScientific` `NNRat.cast` `Rat.ofScientific_nonneg`	—	—

Rat

Definitions

Name	Category	Theorems
`instDistribLattice` 📖	CompOp	—
`instInf` 📖	CompOp	2 math math: `cast_min`, `NNRat.coe_min`
`instLattice` 📖	CompOp	75 math math: `Real.ofCauchy_sup`, `NNRat.abs_coe`, `NumberField.mixedEmbedding.norm_eq_norm`, `coe_nnabs`, `NumberField.FinitePlace.prod_eq_inv_abs_norm`, `Real.ofCauchy_zero`, `NumberField.Units.dirichletUnitTheorem.seq_next`, `Real.of_near`, `Real.ofCauchy_mul`, `Real.cauchy_sub`, `Real.mk_one`, `num_abs_eq_abs_num`, `Real.ofCauchy_nnratCast`, `NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le`, `Real.lt_cauchy`, `finite_rat_abs_sub_lt_one_div_den_sq`, `NumberField.det_basisOfFractionalIdeal_eq_absNorm`, `Real.ofCauchy_sub`, `Real.mk_lt`, `NumberField.Units.norm`, `SimpleGraph.nonuniformWitnesses_spec`, `preimage_cast_uIcc`, `Real.mk_mul`, `Real.cauchy_inv`, `Real.cauchy_nnratCast`, `Real.mk_add`, `AddSubgroup.relIndex_eq_abs_det`, `SimpleGraph.not_isUniform_iff`, `uniformContinuous_abs`, `Real.ofCauchy_natCast`, `Real.cauchy_natCast`, `FractionalIdeal.absNorm_span_singleton`, `Real.ofCauchy_ratCast`, `NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le`, `den_abs_eq_den`, `Real.ofCauchy_intCast`, `Real.ofCauchy_div`, `cast_abs`, `abs_def`, `Real.cauchy_neg`, `Real.mk_const`, `Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul`, `Real.cauchy_intCast`, `Real.mk_zero`, `Real.cauchy_add`, `Real.ofCauchy_add`, `Real.ofCauchy_inv`, `NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr`, `Real.cauchy_zero`, `Real.ofCauchy_neg`, `SimpleGraph.nonuniformWitness_spec`, `infinitePlace_apply`, `Real.mk_inf`, `Real.mk_eq`, `Real.ofCauchy_one`, `NumberField.isUnit_iff_norm`, `FractionalIdeal.abs_det_basis_change`, `AbsoluteValue.real_eq_abs`, `Real.mk_sup`, `sqrt_eq`, `Real.cauchy_one`, `Real.cauchy_ratCast`, `NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr`, `NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply`, `Real.cauchy_mul`, `Real.ringEquivCauchy_apply`, `Real.mk_neg`, `NumberField.InfinitePlace.prod_eq_abs_norm`, `instHasSolidNormRat`, `NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion`, `Real.mk_le`, `Real.ringEquivCauchy_symm_apply_cauchy`, `Real.isCauSeq_iff_lift`, `abs_def'`, `Real.ofCauchy_inf`
`instPartialOrder` 📖	CompOp	19 math math: `padicNorm.instIsAbsoluteValueRat`, `Padic.complete'`, `padicNormE.nonarchimedean'`, `NNRat.floor_coe`, `padicNormE.image'`, `padicNormE.eq_padic_norm'`, `padicNormE.defn`, `padicNormE.add_eq_max_of_ne'`, `instIsOrderedAddMonoid`, `NNRat.mk_natCast`, `Padic.padicNormE.is_norm`, `natFloor_natCast_div_natCast`, `Padic.complete''`, `NNRat.ceil_coe`, `Padic.exi_rat_seq_conv`, `instIsStrictOrderedRing`, `Padic.rat_dense'`, `instArchimedeanRat`, `instStarOrderedRing`
`instPreorder` 📖	CompOp	51 math math: `ProbabilityTheory.tendsto_defaultRatCDF_atBot`, `ProbabilityTheory.tendsto_defaultRatCDF_atTop`, `ProbabilityTheory.IsMeasurableRatCDF.iInf_rat_gt_eq`, `NNRat.mk_zero`, `ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero`, `ProbabilityTheory.monotone_defaultRatCDF`, `preimage_cast_Ioi`, `ProbabilityTheory.IsMeasurableRatCDF.tendsto_atBot_zero`, `Filter.Eventually.ratCast_atBot`, `preimage_cast_Icc`, `instOrderTopology`, `Real.exists_seq_rat_strictAnti_tendsto`, `ProbabilityTheory.IsRatCondKernelCDFAux.mono`, `preimage_cast_Ico`, `ProbabilityTheory.IsRatCondKernelCDF.tendsto_atTop_one`, `instPosMulMono`, `comap_cast_atBot`, `addSubmonoid_closure_range_pow`, `ProbabilityTheory.monotone_preCDF`, `tendsto_ratCast_atBot_iff`, `preimage_cast_Iic`, `ProbabilityTheory.IsRatStieltjesPoint.mono`, `preimage_cast_Ici`, `addSubmonoid_closure_range_mul_self`, `DivisibleHull.qsmul_def`, `ProbabilityTheory.IsRatCondKernelCDF.tendsto_atBot_zero`, `totallyBounded_Icc`, `cast_mono`, `preimage_cast_Iio`, `NNRat.toNNRat_mono`, `ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one`, `ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero`, `NNRat.coe_mono`, `ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt`, `cast_strictMono`, `MeasureTheory.Measure.tendsto_IicSnd_atTop`, `ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt`, `preimage_cast_Ioo`, `DivisibleHull.instIsStrictOrderedModuleRat`, `ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atTop_one`, `MeasureTheory.Measure.tendsto_IicSnd_atBot`, `ProbabilityTheory.iInf_rat_gt_defaultRatCDF`, `ProbabilityTheory.IsRatCondKernelCDF.mono`, `preimage_cast_Ioc`, `comap_cast_atTop`, `Real.exists_seq_rat_strictMono_tendsto`, `Filter.Eventually.ratCast_atTop`, `ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq`, `ProbabilityTheory.IsMeasurableRatCDF.tendsto_atTop_one`, `tendsto_ratCast_atTop_iff`, `LinearOrderedField.toPosSMulStrictMono_rat`
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	—
`instSup` 📖	CompOp	9 math math: `padicNormE.nonarchimedean'`, `padicNorm.nonarchimedean`, `NNRat.coe_max`, `padicNormE.add_eq_max_of_ne'`, `cast_max`, `padicNorm.sub`, `PadicSeq.norm_nonarchimedean`, `padicNorm.add_eq_max_of_ne`, `PadicSeq.add_eq_max_of_ne`
`linearOrder` 📖	CompOp	124 math math: `num_lt_succ_floor_mul_den`, `NNRat.coe_floor`, `PadicInt.isCauSeq_nthHom`, `GenContFract.IntFractPair.coe_stream_nth_rat_eq`, `GenContFract.coe_of_h_rat_eq`, `Real.ofCauchy_sup`, `Padic.complete'`, `HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `PadicSeq.ne_zero_iff_nequiv_zero`, `GenContFract.coe_of_s_rat_eq`, `cast_fract`, `ceil_intCast_div_natCast`, `NNRat.floor_coe`, `GenContFract.of_terminates_iff_of_rat_terminates`, `Padic.exi_rat_seq_conv_cauchy`, `Real.ofCauchy_zero`, `Real.of_near`, `Real.ofCauchy_mul`, `GenContFract.IntFractPair.coe_stream'_rat_eq`, `Real.cauchy_sub`, `Padic.zero_def`, `Real.mk_one`, `GenContFract.IntFractPair.exists_nth_stream_eq_none_of_rat`, `floor_natCast_div_natCast`, `Real.ofCauchy_nnratCast`, `HeightOneSpectrum.adicCompletion.padicEquiv_bijOn`, `Real.lt_cauchy`, `round_cast`, `padicNormE.defn`, `CauSeq.Completion.ofRat_rat`, `Real.ofCauchy_sub`, `Real.mk_lt`, `NNRat.intCeil_cast`, `floor_cast`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `GenContFract.IntFractPair.coe_of_rat_eq`, `GenContFract.coe_of_rat_eq`, `PadicSeq.norm_neg`, `NNRat.coe_ceil`, `Nat.Ioc_filter_modEq_card`, `ceil_natCast_div_natCast`, `Int.Ioc_filter_modEq_card`, `Real.mk_mul`, `PadicSeq.norm_nonarchimedean`, `Real.cauchy_inv`, `PadicSeq.not_equiv_zero_const_of_nonzero`, `Real.cauchy_nnratCast`, `GenContFract.IntFractPair.of_inv_fr_num_lt_num_of_pos`, `Real.mk_add`, `Nat.Ico_filter_modEq_card`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `natFloor_natCast_div_natCast`, `RootPairing.linearIndepOn_root_baseOf`, `GaussianInt.div_def`, `Int.Ico_filter_dvd_card`, `GenContFract.coe_of_s_get?_rat_eq`, `Real.ofCauchy_natCast`, `PadicInt.nthHomSeq_mul`, `fract_inv_num_lt_num_of_pos`, `Padic.mk_eq`, `den_le_and_le_num_le_of_sub_lt_one_div_den_sq`, `Real.cauchy_natCast`, `Padic.complete''`, `Real.ofCauchy_ratCast`, `Nat.coprime_sub_mul_floor_rat_div_of_coprime`, `NNRat.ceil_coe`, `Padic.exi_rat_seq_conv`, `Real.ofCauchy_intCast`, `PadicSeq.not_limZero_const_of_nonzero`, `preimage_cast_uIoc`, `Real.ofCauchy_div`, `HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `RootPairing.eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure`, `floor_def'`, `Real.cauchy_neg`, `uniformSpace_eq`, `Real.mk_const`, `Real.cauchy_intCast`, `Real.mk_zero`, `Real.cauchy_add`, `Real.ofCauchy_add`, `RootPairing.eq_baseOf_iff`, `Real.ofCauchy_inv`, `Real.cauchy_zero`, `Real.ofCauchy_neg`, `Int.Ico_filter_modEq_card`, `Int.Ioc_filter_dvd_eq`, `Real.mk_inf`, `ceil_cast`, `PadicSeq.add_eq_max_of_ne`, `Real.mk_eq`, `Real.ofCauchy_one`, `PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub`, `Real.mk_sup`, `PadicInt.nthHomSeq_add`, `Real.cauchy_one`, `PadicInt.nthHomSeq_one`, `GenContFract.terminates_of_rat`, `Real.cauchy_ratCast`, `Nat.count_modEq_card_eq_ceil`, `PadicSeq.norm_const`, `PadicSeq.norm_one`, `Real.cauchy_mul`, `Real.ringEquivCauchy_apply`, `PadicSeq.norm_zero_iff`, `Real.mk_neg`, `instNonemptySeedRatReal`, `NNRat.intFloor_cast`, `den_intFract`, `Int.mod_nat_eq_sub_mul_floor_rat_div`, `PadicSeq.norm_mul`, `Padic.const_equiv`, `Int.Ico_filter_dvd_eq`, `Real.mk_le`, `Real.ringEquivCauchy_symm_apply_cauchy`, `floor_intCast_div_natCast`, `Real.isCauSeq_iff_lift`, `Real.mk_pos`, `Int.Ioc_filter_dvd_card`, `ceil_def'`, `PadicSeq.eq_zero_iff_equiv_zero`, `Real.ofCauchy_inf`, `niven_fract_angle_div_pi_eq`, `RootPairing.baseOf_root_eq_baseOf_coroot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_def` 📖	mathematical	—	`abs` `instLattice` `addGroup`	—	—
`abs_def'` 📖	mathematical	—	`abs` `instLattice` `addGroup` `instLatticeInt` `Int.instAddGroup` `den_ne_zero` `Int.abs_eq_natAbs`	—	`den_ne_zero` `Int.abs_eq_natAbs` `abs_def`
`den_abs_eq_den` 📖	mathematical	—	`abs` `instLattice` `addGroup`	—	`den_ne_zero` `Int.abs_eq_natAbs` `abs_def'`
`divInt_le_divInt` 📖	—	—	—	—	`sub_eq_add_neg` `ne_of_gt` `neg_mul` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `zero_add`
`div_lt_div_iff_mul_lt_mul` 📖	—	—	—	—	`div_def'` `Nat.cast_one` `mul_one` `one_mul` `divInt_le_divInt`
`instAddLeftMono` 📖	mathematical	—	`AddLeftMono`	—	—
`lt_iff_le_not_ge` 📖	—	—	—	—	—
`lt_one_iff_num_lt_denom` 📖	—	—	—	—	`Nat.cast_one` `mul_one` `one_mul`
`mkRat_neg` 📖	—	—	—	—	`mkRat_neg_iff`
`mkRat_neg_iff` 📖	—	—	—	—	—
`mkRat_nonneg` 📖	—	—	—	—	—
`mkRat_nonneg_iff` 📖	—	—	—	—	—
`mkRat_nonpos` 📖	—	—	—	—	`eq_or_ne` `mkRat_nonpos_iff`
`mkRat_nonpos_iff` 📖	—	—	—	—	—
`mkRat_pos` 📖	—	—	—	—	`mkRat_pos_iff`
`mkRat_pos_iff` 📖	—	—	—	—	—
`num_abs_eq_abs_num` 📖	mathematical	—	`abs` `instLattice` `addGroup` `instLatticeInt` `Int.instAddGroup`	—	`den_ne_zero` `Int.abs_eq_natAbs` `abs_def'`
`num_neg` 📖	—	—	—	—	`lt_iff_lt_of_le_iff_le`
`num_nonpos` 📖	—	—	—	—	`instIsEmptyFalse`
`num_pos` 📖	—	—	—	—	`lt_iff_lt_of_le_iff_le` `num_nonpos`
`ofScientific_nonneg` 📖	—	—	—	—	`ofScientific.eq_1`

---

← Back to Index