Basic

📁 Source: Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

Statistics

Metric	Count
Definitions `padicValInt`, `padicValRat`	2
Theorems `log_ne_padicValNat_succ`, `max_log_padicValNat_succ_eq_log_succ`, `dvd_iff_padicValNat_ne_zero`, `dvd_of_one_le_padicValNat`, `nat_log_eq_padicValNat_iff`, `one_le_padicValNat_of_dvd`, `eq_zero_iff`, `eq_zero_of_not_dvd`, `mul`, `of_nat`, `of_ne_one_ne_zero`, `one`, `self`, `zero`, `padicValInt_dvd`, `padicValInt_dvd_iff`, `padicValInt_mul_eq_succ`, `padicValInt_self`, `div`, `div'`, `div_of_dvd`, `div_pow`, `eq_zero_of_not_dvd`, `maxPowDiv_eq_emultiplicity`, `maxPowDiv_eq_multiplicity`, `mul`, `padicValNat_eq_maxPowDiv`, `pow`, `prime_pow`, `self`, `padicValNat_add_le_self`, `padicValNat_choose`, `padicValNat_choose'`, `padicValNat_dvd_iff`, `padicValNat_dvd_iff_le`, `padicValNat_eq_zero_of_mem_Ioo`, `padicValNat_factorial`, `padicValNat_factorial_le`, `padicValNat_factorial_lt_of_ne_zero`, `padicValNat_factorial_mul`, `padicValNat_factorial_mul_add`, `padicValNat_le_nat_log`, `padicValNat_mul_div_factorial`, `padicValNat_mul_pow_left`, `padicValNat_mul_pow_right`, `padicValNat_prime_prime_pow`, `padicValNat_primes`, `padicValNat_self`, `add_eq_min`, `add_eq_of_lt`, `defn`, `div`, `finite_int_prime_iff`, `inv`, `le_padicValRat_add_of_le`, `lt_add_of_lt`, `lt_sum_of_lt`, `min_le_padicValRat_add`, `mul`, `multiplicity_sub_multiplicity`, `neg`, `of_int`, `of_int_multiplicity`, `of_nat`, `one`, `padicValRat_le_padicValRat_iff`, `pow`, `self`, `self_pow_inv`, `sum_pos_of_pos`, `zero`, `padicValRat_def`, `padicValRat_of_nat`, `pow_padicValNat_dvd`, `pow_succ_padicValNat_not_dvd`, `range_pow_padicValNat_subset_divisors`, `range_pow_padicValNat_subset_divisors'`, `sub_one_mul_padicValNat_choose_eq_sub_sum_digits`, `sub_one_mul_padicValNat_choose_eq_sub_sum_digits'`, `sub_one_mul_padicValNat_factorial`, `sub_one_mul_padicValNat_factorial_lt_of_ne_zero`, `zero_le_padicValRat_of_nat`	82
Total	84

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`log_ne_padicValNat_succ` 📖	—	—	—	—	`log_eq_iff` `instCharZero` `instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `mul_one` `lt_of_le_of_ne'` `pow_succ_padicValNat_not_dvd` `fact_prime_two` `dvd_of_eq` `pow_padicValNat_dvd`
`max_log_padicValNat_succ_eq_log_succ` 📖	mathematical	—	`log` `padicValNat`	—	`le_antisymm` `max_le` `le_log_of_pow_le` `Prime.one_lt` `Fact.out` `pow_log_le_add_one` `padicValNat_le_nat_log` `le_max_iff` `not_le` `lt_pow_of_log_lt` `pow_log_le_self` `padicValNat.prime_pow` `le_refl`

(root)

Definitions

Name	Category	Theorems
`padicValInt` 📖	CompOp	15 math math: `padicValInt.eq_zero_of_not_dvd`, `padicValInt.zero`, `padicValInt.eq_zero_iff`, `padicValInt.one`, `padicValInt_dvd_iff`, `padicValInt_self`, `padicValInt_mul_eq_succ`, `padicValRat.of_int`, `Padic.valuation_intCast`, `padicValRat_def`, `padicValInt.self`, `padicValInt.mul`, `padicValInt.of_nat`, `padicValInt.of_ne_one_ne_zero`, `padicValInt_dvd`
`padicValRat` 📖	CompOp	23 math math: `padicValRat.padicValRat_le_padicValRat_iff`, `padicValRat.neg`, `padicValRat.zero`, `padicValRat.self_pow_inv`, `padicValRat.of_int_multiplicity`, `padicValRat.min_le_padicValRat_add`, `padicNorm.eq_zpow_of_nonzero`, `padicValRat_two_harmonic`, `padicValRat.one`, `padicValRat.of_int`, `padicValRat.multiplicity_sub_multiplicity`, `padicValRat_def`, `padicValRat.of_nat`, `Padic.valuation_ratCast`, `padicValRat.defn`, `padicValRat.add_eq_min`, `padicValRat_of_nat`, `padicValRat.inv`, `padicValRat.pow`, `padicValRat.div`, `padicValRat.mul`, `zero_le_padicValRat_of_nat`, `padicValRat.self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_iff_padicValNat_ne_zero` 📖	—	—	—	—	`one_le_padicValNat_of_dvd` `padicValNat.eq_zero_of_not_dvd`
`dvd_of_one_le_padicValNat` 📖	—	`padicValNat`	—	—	`lt_irrefl` `lt_of_lt_of_le` `zero_lt_one` `Nat.instZeroLEOneClass` `padicValNat.eq_zero_of_not_dvd`
`nat_log_eq_padicValNat_iff` 📖	mathematical	—	`Nat.log` `padicValNat` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.log_eq_iff` `Fact.out` `Nat.Prime.one_lt'` `pow_padicValNat_dvd`
`one_le_padicValNat_of_dvd` 📖	mathematical	—	`padicValNat`	—	`WithTop.coe_le_coe` `ENat.some_eq_coe` `padicValNat_eq_emultiplicity` `pow_dvd_iff_le_emultiplicity` `pow_one`
`padicValInt_dvd` 📖	mathematical	—	`Monoid.toNatPow` `Int.instMonoid` `padicValInt`	—	`padicValInt_dvd_iff` `le_rfl`
`padicValInt_dvd_iff` 📖	mathematical	—	`Monoid.toNatPow` `Int.instMonoid` `padicValInt`	—	`padicValInt.eq_1` `padicValNat_dvd_iff` `Int.natCast_dvd`
`padicValInt_mul_eq_succ` 📖	mathematical	—	`padicValInt`	—	`padicValInt.mul` `Nat.Prime.ne_zero` `Fact.out` `padicValInt.of_nat` `padicValNat_self`
`padicValInt_self` 📖	mathematical	—	`padicValInt`	—	`padicValInt.self` `Nat.Prime.one_lt` `Fact.out`
`padicValNat_add_le_self` 📖	mathematical	—	`padicValNat`	—	`padicValNat_le_nat_log` `Nat.log_lt_self` `padicValNat.mul` `padicValNat_self` `Nat.Prime.two_le` `Fact.out` `padicValNat.eq_zero_of_not_dvd`
`padicValNat_choose` 📖	mathematical	`Nat.log`	`padicValNat` `Nat.choose` `Finset.card` `Finset.filter` `Monoid.toNatPow` `Nat.instMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Nat.Prime.emultiplicity_choose` `Fact.out` `padicValNat_eq_emultiplicity` `Nat.choose_ne_zero`
`padicValNat_choose'` 📖	mathematical	`Nat.log`	`padicValNat` `Nat.choose` `Finset.card` `Finset.filter` `Monoid.toNatPow` `Nat.instMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder`	—	`Nat.Prime.emultiplicity_choose'` `Fact.out` `padicValNat_eq_emultiplicity` `Nat.choose_ne_zero`
`padicValNat_dvd_iff` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `padicValNat`	—	`eq_or_ne` `dvd_zero` `padicValNat_dvd_iff_le`
`padicValNat_dvd_iff_le` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `padicValNat`	—	`pow_dvd_iff_le_emultiplicity` `padicValNat_eq_emultiplicity` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`padicValNat_eq_zero_of_mem_Ioo` 📖	mathematical	`Set` `Set.instMembership` `Set.Ioo` `Nat.instPreorder`	`padicValNat`	—	`padicValNat.eq_zero_of_not_dvd`
`padicValNat_factorial` 📖	mathematical	`Nat.log`	`padicValNat` `Nat.factorial` `Finset.sum` `Nat.instAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.Prime.emultiplicity_factorial` `Fact.out` `padicValNat_eq_emultiplicity` `Nat.factorial_ne_zero`
`padicValNat_factorial_le` 📖	mathematical	—	`padicValNat` `Nat.factorial`	—	`padicValNat.one` `le_of_lt` `padicValNat_factorial_lt_of_ne_zero`
`padicValNat_factorial_lt_of_ne_zero` 📖	mathematical	—	`padicValNat` `Nat.factorial`	—	`lt_of_le_of_lt` `one_mul` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `Nat.Prime.one_lt` `Fact.elim` `sub_one_mul_padicValNat_factorial_lt_of_ne_zero`
`padicValNat_factorial_mul` 📖	mathematical	—	`padicValNat` `Nat.factorial`	—	`Nat.cast_injective` `padicValNat_eq_emultiplicity` `Nat.factorial_ne_zero` `Nat.cast_add` `Nat.Prime.emultiplicity_factorial_mul` `Fact.out`
`padicValNat_factorial_mul_add` 📖	mathematical	—	`padicValNat` `Nat.factorial`	—	`add_zero` `Nat.factorial_succ` `padicValNat.mul` `Nat.factorial_ne_zero` `padicValNat_eq_zero_of_mem_Ioo` `add_lt_add_iff_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `zero_add`
`padicValNat_le_nat_log` 📖	mathematical	—	`padicValNat` `Nat.log`	—	`padicValNat.zero` `Nat.log_zero_right` `Nat.log_zero_left` `Nat.instCanonicallyOrderedAdd` `zero_add` `Nat.log_one_left` `Unique.instSubsingleton` `Nat.le_log_of_pow_le` `pow_padicValNat_dvd`
`padicValNat_mul_div_factorial` 📖	mathematical	—	`padicValNat` `Nat.factorial`	—	`padicValNat_factorial_mul_add` `Nat.Prime.pos` `Fact.out`
`padicValNat_mul_pow_left` 📖	mathematical	—	`padicValNat` `Monoid.toNatPow` `Nat.instMonoid`	—	`padicValNat.mul` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `padicValNat.prime_pow` `padicValNat_prime_prime_pow` `add_zero`
`padicValNat_mul_pow_right` 📖	mathematical	—	`padicValNat` `Monoid.toNatPow` `Nat.instMonoid`	—	`mul_comm` `padicValNat_mul_pow_left`
`padicValNat_prime_prime_pow` 📖	mathematical	—	`padicValNat` `Monoid.toNatPow` `Nat.instMonoid`	—	`padicValNat.pow` `Nat.Prime.ne_zero` `Fact.elim` `padicValNat_primes` `MulZeroClass.mul_zero`
`padicValNat_primes` 📖	mathematical	—	`padicValNat`	—	`padicValNat.eq_zero_of_not_dvd` `Nat.prime_dvd_prime_iff_eq` `Fact.out`
`padicValNat_self` 📖	mathematical	—	`padicValNat`	—	`padicValNat_def` `Nat.Prime.ne_zero` `Fact.out` `multiplicity_self` `Nat.instIsCancelMulZero`
`padicValRat_def` 📖	mathematical	—	`padicValRat` `padicValInt` `padicValNat`	—	—
`padicValRat_of_nat` 📖	mathematical	—	`padicValNat` `padicValRat`	—	`padicValRat.of_nat`
`pow_padicValNat_dvd` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `padicValNat`	—	`eq_or_ne` `padicValNat.zero` `pow_zero` `Unique.instSubsingleton` `one_pow` `pow_dvd_of_le_multiplicity` `padicValNat_def'` `le_refl`
`pow_succ_padicValNat_not_dvd` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `padicValNat`	—	`padicValNat_dvd_iff_le` `not_le`
`range_pow_padicValNat_subset_divisors` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finset.image` `Monoid.toNatPow` `Nat.instMonoid` `Finset.range` `padicValNat` `Nat.divisors`	—	`Nat.mem_divisors` `Dvd.dvd.trans` `pow_dvd_pow` `pow_padicValNat_dvd`
`range_pow_padicValNat_subset_divisors'` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finset.image` `Monoid.toNatPow` `Nat.instMonoid` `Finset.range` `padicValNat` `Finset.erase` `Nat.divisors`	—	`eq_or_ne` `padicValNat.zero` `Nat.divisors_zero` `Finset.erase_eq_of_notMem` `Finset.instReflSubset` `Finset.mem_erase` `Nat.mem_divisors` `LT.lt.ne'` `Nat.Prime.one_lt` `Fact.out` `Dvd.dvd.trans` `pow_dvd_pow` `pow_padicValNat_dvd`
`sub_one_mul_padicValNat_choose_eq_sub_sum_digits` 📖	mathematical	—	`padicValNat` `Nat.choose` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.digits`	—	`sub_one_mul_padicValNat_choose_eq_sub_sum_digits'`
`sub_one_mul_padicValNat_choose_eq_sub_sum_digits'` 📖	mathematical	—	`padicValNat` `Nat.choose` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.digits`	—	`Nat.choose_eq_factorial_div_factorial` `padicValNat.div_of_dvd` `Nat.factorial_mul_factorial_dvd_factorial` `padicValNat.mul` `Nat.factorial_ne_zero` `sub_one_mul_padicValNat_factorial` `Nat.digit_sum_le` `add_comm` `tsub_tsub_assoc` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `zero_add`
`sub_one_mul_padicValNat_factorial` 📖	mathematical	—	`padicValNat` `Nat.factorial` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.digits`	—	`padicValNat_factorial` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `zero_add` `Finset.sum_Ico_add'` `Nat.instIsOrderedCancelAddMonoid` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.Ico_zero_eq_range` `Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits`
`sub_one_mul_padicValNat_factorial_lt_of_ne_zero` 📖	mathematical	—	`padicValNat` `Nat.factorial`	—	`sub_one_mul_padicValNat_factorial` `Nat.digits_ne_nil_iff_ne_zero` `Nat.getLast_digit_ne_zero` `Nat.digit_sum_le`
`zero_le_padicValRat_of_nat` 📖	mathematical	—	`padicValRat`	—	`padicValRat.of_nat` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing`

padicValInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_iff` 📖	mathematical	—	`padicValInt`	—	`eq_1` `padicValNat.eq_zero_iff`
`eq_zero_of_not_dvd` 📖	mathematical	—	`padicValInt`	—	—
`mul` 📖	mathematical	—	`padicValInt`	—	`padicValNat.mul`
`of_nat` 📖	mathematical	—	`padicValInt` `padicValNat`	—	—
`of_ne_one_ne_zero` 📖	mathematical	—	`padicValInt` `multiplicity` `Int.instMonoid`	—	`eq_1` `padicValNat_def'` `Int.multiplicity_natAbs`
`one` 📖	mathematical	—	`padicValInt`	—	`Int.natAbs_of_isUnit` `padicValNat.one`
`self` 📖	mathematical	—	`padicValInt`	—	`of_nat` `padicValNat.self`
`zero` 📖	mathematical	—	`padicValInt`	—	`padicValNat.zero`

padicValNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	—	`padicValNat`	—	`div_of_dvd` `padicValNat_self`
`div'` 📖	mathematical	—	`padicValNat`	—	`div_of_dvd` `eq_zero_of_not_dvd` `Nat.Prime.coprime_iff_not_dvd` `Fact.out`
`div_of_dvd` 📖	mathematical	—	`padicValNat`	—	`eq_or_ne` `zero` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `mul_ne_zero_iff` `IsDomain.to_noZeroDivisors` `Nat.instIsDomain` `mul_comm` `Ne.bot_lt` `mul`
`div_pow` 📖	mathematical	`Monoid.toNatPow` `Nat.instMonoid`	`padicValNat`	—	`div_of_dvd` `prime_pow`
`eq_zero_of_not_dvd` 📖	mathematical	—	`padicValNat`	—	`eq_zero_iff`
`maxPowDiv_eq_emultiplicity` 📖	mathematical	—	`ENat` `ENat.instNatCast` `Nat.maxPowDiv` `emultiplicity` `Nat.instMonoid`	—	`emultiplicity_eq_of_dvd_of_not_dvd` `Nat.maxPowDiv.pow_dvd` `Nat.maxPowDiv.le_of_dvd` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass`
`maxPowDiv_eq_multiplicity` 📖	mathematical	`FiniteMultiplicity` `Nat.instMonoid`	`Nat.maxPowDiv` `multiplicity`	—	`maxPowDiv_eq_emultiplicity` `FiniteMultiplicity.emultiplicity_eq_multiplicity`
`mul` 📖	mathematical	—	`padicValNat`	—	`Nat.cast_zero` `Rat.instCharZero` `Int.instCharZero` `padicValRat.mul`
`padicValNat_eq_maxPowDiv` 📖	mathematical	—	`padicValNat` `Nat.maxPowDiv`	—	`padicValNat_def'` `LT.lt.ne'` `maxPowDiv_eq_multiplicity` `Nat.finiteMultiplicity_iff` `Mathlib.Tactic.Push.not_and_or_eq` `Nat.maxPowDiv.go.eq_1` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_le_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.maxPowDiv.zero_base` `zero` `Nat.maxPowDiv.zero`
`pow` 📖	mathematical	—	`padicValNat` `Monoid.toNatPow` `Nat.instMonoid`	—	`Int.instCharZero` `padicValRat_of_nat` `Nat.cast_pow` `Nat.cast_mul` `padicValRat.pow` `Nat.cast_ne_zero` `Rat.instCharZero`
`prime_pow` 📖	mathematical	—	`padicValNat` `Monoid.toNatPow` `Nat.instMonoid`	—	`pow` `Nat.Prime.ne_zero` `Fact.out` `padicValNat_self` `mul_one`
`self` 📖	mathematical	—	`padicValNat`	—	`padicValNat_def'` `LT.lt.ne'` `ne_zero_of_lt` `multiplicity_self` `Nat.instIsCancelMulZero`

padicValRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_min` 📖	mathematical	—	`padicValRat`	—	`min_le_padicValRat_add` `ne_of_eq_of_ne` `add_neg_cancel_right` `neg` `add_comm`
`add_eq_of_lt` 📖	—	`padicValRat`	—	—	`add_eq_min` `ne_of_lt` `min_eq_left` `le_of_lt`
`defn` 📖	mathematical	—	`padicValRat` `multiplicity` `Int.instMonoid`	—	`Rat.mk_denom_ne_zero_of_ne_zero` `multiplicity_sub_multiplicity` `Nat.Prime.ne_one` `Fact.out` `multiplicity_mul` `Int.instIsCancelMulZero` `Nat.prime_iff_prime_int` `IsDomain.to_noZeroDivisors` `Int.instIsDomain` `Nat.cast_add` `Int.natCast_multiplicity` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add`
`div` 📖	mathematical	—	`padicValRat`	—	`div_eq_mul_inv` `mul` `inv_ne_zero` `inv` `sub_eq_add_neg`
`finite_int_prime_iff` 📖	mathematical	—	`FiniteMultiplicity` `Int.instMonoid`	—	`Nat.Prime.ne_one` `Fact.out`
`inv` 📖	mathematical	—	`padicValRat`	—	`inv_zero` `zero` `neg_zero` `eq_neg_iff_add_eq_zero` `mul` `inv_ne_zero` `inv_mul_cancel₀` `one`
`le_padicValRat_add_of_le` 📖	—	`padicValRat`	—	—	`zero` `zero_add` `add_zero` `Rat.num_ne_zero` `Nat.cast_zero` `Int.instCharZero` `Rat.add_num_den` `Rat.mk_num_ne_zero_of_ne_zero` `padicValRat_le_padicValRat_iff` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `Int.instIsDomain` `emultiplicity_le_emultiplicity_iff` `mul_left_comm` `emultiplicity_mul` `Int.instIsCancelMulZero` `Nat.prime_iff_prime_int` `Fact.out` `add_mul` `Distrib.rightDistribClass` `le_min` `add_comm` `le_refl` `mul_assoc` `le_imp_le_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `min_le_emultiplicity_add`
`lt_add_of_lt` 📖	—	`padicValRat`	—	—	`lt_of_lt_of_le` `lt_min` `min_le_padicValRat_add`
`lt_sum_of_lt` 📖	mathematical	`Finset.Nonempty` `padicValRat`	`Finset.sum` `Rat.addCommMonoid`	—	`Finset.Nonempty.cons_induction` `Finset.sum_singleton` `Finset.cons_eq_insert` `Finset.sum_insert` `lt_add_of_lt` `ne_of_gt` `add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Rat.instAddLeftMono` `Finset.sum_pos` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Rat.instIsStrictOrderedRing` `Finset.mem_insert`
`min_le_padicValRat_add` 📖	mathematical	—	`padicValRat`	—	`le_total` `min_eq_left` `le_padicValRat_add_of_le` `min_eq_right` `add_comm`
`mul` 📖	mathematical	—	`padicValRat`	—	`Rat.mul_eq_mkRat` `Rat.mkRat_eq_divInt` `Nat.cast_mul` `Nat.prime_iff_prime_int` `Fact.out` `defn` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `Rat.isDomain` `multiplicity_mul` `Int.instIsCancelMulZero` `Int.instIsDomain` `Nat.cast_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_pf_add_gt`
`multiplicity_sub_multiplicity` 📖	mathematical	—	`padicValRat` `multiplicity` `Int.instMonoid` `Nat.instMonoid`	—	`eq_1` `padicValInt.of_ne_one_ne_zero` `Rat.num_ne_zero` `padicValNat_def'` `Rat.den_ne_zero`
`neg` 📖	mathematical	—	`padicValRat`	—	—
`of_int` 📖	mathematical	—	`padicValRat` `padicValInt`	—	`padicValNat.one` `Nat.cast_zero` `sub_zero`
`of_int_multiplicity` 📖	mathematical	—	`padicValRat` `multiplicity` `Int.instMonoid`	—	`of_int` `padicValInt.of_ne_one_ne_zero`
`of_nat` 📖	mathematical	—	`padicValRat` `padicValNat`	—	`padicValInt.of_nat` `padicValNat.one` `Nat.cast_zero` `sub_zero`
`one` 📖	mathematical	—	`padicValRat`	—	`padicValInt.one` `Nat.cast_zero` `padicValNat.one` `sub_self`
`padicValRat_le_padicValRat_iff` 📖	mathematical	—	`padicValRat` `Monoid.toNatPow` `Int.instMonoid`	—	`finite_int_prime_iff` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `Int.instIsDomain` `defn` `Rat.divInt_ne_zero_of_ne_zero` `sub_le_iff_le_add'` `Int.instAddLeftMono` `add_sub_assoc` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `Int.instZeroLEOneClass` `Int.instCharZero` `multiplicity_mul` `Int.instIsCancelMulZero` `Nat.prime_iff_prime_int` `Fact.out` `add_comm` `FiniteMultiplicity.multiplicity_le_multiplicity_iff`
`pow` 📖	mathematical	—	`padicValRat`	—	`pow_zero` `one` `Nat.cast_zero` `MulZeroClass.zero_mul` `pow_succ'` `mul` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `Rat.isDomain` `Nat.cast_add` `Nat.cast_one` `add_mul` `Distrib.rightDistribClass` `one_mul` `add_comm`
`self` 📖	mathematical	—	`padicValRat`	—	`of_nat` `padicValNat.self` `Nat.cast_one`
`self_pow_inv` 📖	mathematical	—	`padicValRat`	—	`inv` `pow` `Nat.cast_ne_zero` `Rat.instCharZero` `Nat.Prime.ne_zero` `Fact.elim` `self` `Nat.Prime.one_lt` `mul_one`
`sum_pos_of_pos` 📖	mathematical	`padicValRat`	`Finset.sum` `Rat.addCommMonoid` `Finset.range`	—	`Finset.sum_range_succ` `zero_add` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `lt_of_lt_of_le` `lt_min` `lt_trans` `min_le_padicValRat_add`
`zero` 📖	mathematical	—	`padicValRat`	—	`padicValInt.zero` `Nat.cast_zero` `padicValNat.one` `sub_self`

---

← Back to Index