Documentation Verification Report

Ostrowski

📁 Source: Mathlib/NumberTheory/Ostrowski.lean

Statistics

Metric	Count
Definitions `padic`, `real`	2
Theorems `apply_le_sum_digits`, `eq_on_nat_iff_eq`, `eq_one_of_not_dvd`, `equiv_padic_of_bounded`, `equiv_real_of_unbounded`, `equiv_real_or_padic`, `exists_minimal_nat_zero_lt_and_lt_one`, `exists_nat_rpow_iff_isEquiv`, `exists_pos_eq_pow_neg`, `is_prime_of_minimal_nat_zero_lt_and_lt_one`, `le_pow_log`, `not_real_isEquiv_padic`, `one_lt_of_not_bounded`, `padic_eq_padicNorm`, `padic_le_one`, `real_eq_abs`	16
Total	18

Rat.AbsoluteValue

Definitions

Name	Category	Theorems
`padic` 📖	CompOp	5 math math: `equiv_real_or_padic`, `padic_eq_padicNorm`, `padic_le_one`, `equiv_padic_of_bounded`, `not_real_isEquiv_padic`
`real` 📖	CompOp	4 math math: `equiv_real_of_unbounded`, `equiv_real_or_padic`, `real_eq_abs`, `not_real_isEquiv_padic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_le_sum_digits` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instAdd` `Real.instZero` `Real.instMul` `Real.instNatCast` `Monoid.toPow` `Real.instMonoid` `Nat.digits`	—	`lt_of_le_of_lt` `AbsoluteValue.apply_nat_le_self` `Real.instIsDomain` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.digits_lt_base` `Nat.ofDigits_digits` `Nat.ofDigits_eq_sum_mapIdx` `Nat.cast_list_sum` `AbsoluteValue.listSum_le` `List.sum_le_sum` `covariant_swap_add_of_covariant_add` `Nat.cast_mul` `Nat.cast_pow` `map_mul` `AbsoluteValue.mulHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Rat.nontrivial` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `LT.lt.le` `zero_add` `pow_nonneg` `IsOrderedRing.toPosMulMono` `AbsoluteValue.nonneg`
`eq_on_nat_iff_eq` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Real` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike`	—	`AbsoluteValue.ext` `Rat.num_div_den` `map_div₀` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `Rat.nontrivial` `AbsoluteValue.eq_on_nat_iff_eq_on_int` `Real.instIsOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`
`eq_one_of_not_dvd` 📖	mathematical	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instOne` `Real.instLT` `Real.instZero`	`DFunLike.coe` `AbsoluteValue` `Real` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instOne`	—	`le_antisymm` `Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `IsCoprime.pow` `Nat.Coprime.isCoprime` `Nat.Prime.coprime_iff_not_dvd` `is_prime_of_minimal_nat_zero_lt_and_lt_one` `Real.rpow_natCast` `Real.rpow_lt_rpow_of_exponent_gt` `Nat.cast_add` `Nat.cast_one` `lt_add_of_le_of_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.le_ceil` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.rpow_le_rpow_of_exponent_ge` `LT.lt.le` `one_div` `Real.log_inv` `neg_div` `div_le_div₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_lt` `Mathlib.Meta.Positivity.log_pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `le_refl` `Real.log_neg` `lt_sup_iff` `sup_lt_iff` `neg_le_neg` `Real.log_le_log` `Real.rpow_logb` `LT.lt.ne` `one_half_pos` `lt_irrefl` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `Rat.nontrivial` `Nat.cast_pow` `Int.cast_pow` `Int.cast_natCast` `Int.cast_one` `AbsoluteValue.add_le'` `map_mul` `AbsoluteValue.mulHomClass` `map_pow` `add_le_add` `covariant_swap_add_of_covariant_add` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `AbsoluteValue.apply_natAbs_eq` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `NonnegHomClass.apply_nonneg` `AbsoluteValue.nonnegHomClass` `one_mul` `AbsoluteValue.pos` `Nat.cast_ne_zero` `Rat.instCharZero` `dvd_zero` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `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` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.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` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.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` `le_sup_left` `le_sup_right`
`equiv_padic_of_bounded` 📖	mathematical	`AbsoluteValue.IsNontrivial` `Rat.semiring` `Real` `Real.semiring` `Real.partialOrder` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `Real.instOne`	`ExistsUnique` `Fact` `Nat.Prime` `AbsoluteValue.IsEquiv` `Rat.semiring` `Real` `Real.semiring` `Real.partialOrder` `padic`	—	`exists_minimal_nat_zero_lt_and_lt_one` `is_prime_of_minimal_nat_zero_lt_and_lt_one` `exists_pos_eq_pow_neg` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `inv_ne_zero` `LT.lt.ne'` `eq_or_ne` `CharP.cast_eq_zero` `CharP.ofCharZero` `Rat.instCharZero` `AbsoluteValue.map_zero` `Real.zero_rpow` `Nat.exists_eq_pow_mul_and_not_dvd` `Nat.Prime.ne_one` `Nat.cast_mul` `Nat.cast_pow` `map_mul` `AbsoluteValue.mulHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `Rat.nontrivial` `eq_one_of_not_dvd` `padicNorm.padicNorm_p_of_prime` `Rat.cast_inv` `RCLike.charZero_rclike` `Rat.cast_natCast` `inv_pow` `Nat.cast_nonneg` `Real.instIsOrderedRing` `neg_mul` `mul_one` `padicNorm.nat_eq_one_iff` `Rat.cast_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Fact.elim` `Nat.Prime.coprime_iff_not_dvd` `Nat.coprime_primes` `Real.one_rpow`
`equiv_real_of_unbounded` 📖	mathematical	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instOne`	`AbsoluteValue.IsEquiv` `Rat.semiring` `Real` `Real.semiring` `Real.partialOrder` `real`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `CharP.cast_eq_zero` `CharP.ofCharZero` `Rat.instCharZero` `AbsoluteValue.map_zero` `Real.instZeroLEOneClass` `Nat.cast_one` `AbsoluteValue.map_one` `Real.instIsDomain` `Rat.nontrivial` `instReflLe` `exists_nat_rpow_iff_isEquiv` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.logb_pos` `Nat.one_lt_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `RCLike.charZero_rclike` `one_lt_of_not_bounded` `lt_trichotomy` `Real.instNontrivial` `AbsoluteValue.monoidWithZeroHomClass` `ne_zero_of_lt` `LT.lt.ne'` `Int.cast_natCast` `ne_of_not_le` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `NonnegHomClass.apply_nonneg` `AbsoluteValue.nonnegHomClass` `Real.zero_rpow` `Real.one_rpow` `real_eq_abs` `Nat.abs_cast` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.cast_natCast` `Real.rpow_inv_eq` `Nat.cast_nonneg` `Real.logb_ne_zero_of_pos_of_ne_one` `lt_of_not_ge` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `Real.rpow_logb` `map_pos_of_ne_zero` `MulRingNormClass.toAddGroupNormClass` `AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`
`equiv_real_or_padic` 📖	mathematical	`AbsoluteValue.IsNontrivial` `Rat.semiring` `Real` `Real.semiring` `Real.partialOrder`	`AbsoluteValue` `Real` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.instSetoid` `real` `ExistsUnique` `Fact` `Nat.Prime` `padic`	—	`equiv_padic_of_bounded` `equiv_real_of_unbounded`
`exists_minimal_nat_zero_lt_and_lt_one` 📖	mathematical	`AbsoluteValue.IsNontrivial` `Rat.semiring` `Real` `Real.semiring` `Real.partialOrder` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `AbsoluteValue.funLike` `Real.instOne`	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instOne`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instIsOrderedRing` `Real.instNontrivial` `Iff.not_left` `AbsoluteValue.isNontrivial_iff_ne_trivial` `eq_on_nat_iff_eq` `eq_or_ne` `CharP.cast_eq_zero` `CharP.ofCharZero` `Rat.instCharZero` `AbsoluteValue.map_zero` `AbsoluteValue.trivial_apply` `map_pos_of_ne_zero` `Real.instIsOrderedAddMonoid` `MulRingNormClass.toAddGroupNormClass` `AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain` `Rat.nontrivial` `Real.instIsDomain` `Nat.cast_ne_zero` `lt_of_le_of_ne` `Nat.sInf_mem` `Nat.sInf_le`
`exists_nat_rpow_iff_isEquiv` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instPow` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `AbsoluteValue.IsEquiv`	—	`AbsoluteValue.isEquiv_iff_exists_rpow_eq` `Rat.num_div_den` `map_div₀` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `Rat.nontrivial` `Real.div_rpow` `NonnegHomClass.apply_nonneg` `AbsoluteValue.nonnegHomClass` `AbsoluteValue.apply_natAbs_eq` `Real.instIsOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`
`exists_pos_eq_pow_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instOne`	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instPow` `Real.instNatCast` `Real.instNeg`	—	`is_prime_of_minimal_nat_zero_lt_and_lt_one` `Left.neg_pos_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.logb_neg` `Nat.cast_one` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.Prime.one_lt` `neg_neg` `Real.rpow_logb` `Nat.cast_zero` `Nat.Prime.pos` `Nat.Prime.ne_one`
`is_prime_of_minimal_nat_zero_lt_and_lt_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instOne`	`Nat.Prime`	—	`Nat.irreducible_iff_nat_prime` `Nat.isUnit_iff` `Nat.cast_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `Rat.nontrivial` `mul_ne_zero_iff` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `lt_self_iff_false` `map_zero` `AbsoluteValue.zeroHomClass` `Nat.cast_zero` `lt_mul_of_one_lt_right` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `lt_mul_of_one_lt_left` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_not_gt` `Function.mt` `LT.lt.not_ge` `map_pos_of_ne_zero` `Real.instIsOrderedAddMonoid` `MulRingNormClass.toAddGroupNormClass` `AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain` `Real.instIsOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Rat.instCharZero` `LT.lt.false` `LE.le.trans_lt` `one_le_mul_of_one_le_of_one_le` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `map_mul` `AbsoluteValue.mulHomClass` `Nat.cast_mul`
`le_pow_log` 📖	mathematical	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instOne`	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instPow` `Real.logb` `Real.instNatCast`	—	`one_mul` `Filter.Tendsto.mul_const` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `le_of_tendsto_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_const_nhds` `Filter.eventually_atTop` `ne_zero_of_lt`
`not_real_isEquiv_padic` 📖	mathematical	—	`AbsoluteValue.IsEquiv` `Rat.semiring` `Real` `Real.semiring` `Real.partialOrder` `real` `padic`	—	`AbsoluteValue.isEquiv_iff_exists_rpow_eq` `LT.lt.ne'` `Nat.instAtLeastTwoHAddOfNat` `LE.le.trans_lt` `padic_le_one` `Real.one_lt_rpow` `one_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `real_eq_abs` `Nat.abs_ofNat` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.cast_ofNat`
`one_lt_of_not_bounded` 📖	mathematical	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Real.instOne`	`Real` `Real.instLT` `Real.instOne` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `apply_le_sum_digits` `List.sum_le_sum` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `le_refl` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `NonnegHomClass.apply_nonneg` `AbsoluteValue.nonnegHomClass` `mul_le_of_le_one_right` `le_of_lt` `Nat.cast_pos'` `NeZero.charZero_one` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `pow_le_one₀` `List.sum_replicate` `nsmul_eq_mul` `mul_comm` `Nat.length_digits` `ne_zero_of_lt` `Nat.cast_add_one` `mul_le_mul_of_nonneg_left` `add_le_add_left` `Real.natLog_le_logb` `eq_or_ne` `CharP.cast_eq_zero` `CharP.ofCharZero` `Rat.instCharZero` `AbsoluteValue.map_zero` `Real.logb_nonneg` `Nat.one_lt_cast` `Nat.cast_one` `Ne.bot_lt` `Nat.cast_pow` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `Rat.nontrivial` `Real.rpow_natCast` `Real.rpow_rpow_inv` `ne_of_gt` `Real.rpow_le_rpow` `one_le_pow₀` `Nat.instZeroLEOneClass` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.logb_pow` `mul_pos` `Right.add_pos_of_nonneg_of_pos` `mul_nonneg` `Real.instNontrivial` `add_le_add_right` `Nat.one_le_cast` `Real.mul_rpow` `mul_assoc` `add_mul` `Distrib.rightDistribClass` `one_mul` `AbsoluteValue.map_one` `instReflLe` `le_of_tendsto_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Filter.atTop_neBot` `instIsDirectedOrder` `instArchimedeanNat` `tendsto_const_nhds` `mul_one` `Real.logb_pos` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `add_pos'` `Filter.eventually_atTop`
`padic_eq_padicNorm` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Real` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `padic` `Real.instRatCast` `padicNorm`	—	—
`padic_le_one` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `padic` `Real.instOne`	—	`Nat.cast_one` `Real.instIsStrictOrderedRing` `padicNorm.of_int`
`real_eq_abs` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Real` `Rat.semiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `real` `Real.instRatCast` `abs` `Rat.instLattice` `Rat.addGroup`	—	`Rat.cast_abs` `Real.instIsStrictOrderedRing`

---

← Back to Index