Int

📁 Source: Mathlib/NumberTheory/Harmonic/Int.lean

Statistics

Metric	Count
Definitions	0
Theorems harmonic_not_int, harmonic_pos, padicNorm_two_harmonic, padicValRat_two_harmonic	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonic_not_int 📖	mathematical	—	harmonic	—	padicNorm.not_int_of_not_padic_int Nat.fact_prime_two padicNorm.eq_zpow_of_nonzero LT.lt.ne' harmonic_pos ne_zero_of_lt padicValRat_two_harmonic neg_neg zpow_natCast one_lt_pow₀ Rat.instZeroLEOneClass Rat.instPosMulMono one_lt_two NeZero.charZero_one Rat.instCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Rat.instAddLeftMono Nat.instAtLeastTwoHAddOfNat Nat.log_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
harmonic_pos 📖	mathematical	—	harmonic	—	Finset.sum_pos IsStrictOrderedRing.toIsOrderedCancelAddMonoid Rat.instIsStrictOrderedRing inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Finset.nonempty_range_iff
padicNorm_two_harmonic 📖	mathematical	—	Norm.norm Padic Nat.fact_prime_two Padic.instNorm DivisionRing.toRatCast NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Padic.normedField harmonic Real Monoid.toNatPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Nat.log	—	Nat.fact_prime_two Nat.instAtLeastTwoHAddOfNat Padic.eq_padicNorm padicNorm.eq_zpow_of_nonzero LT.lt.ne' harmonic_pos padicValRat_two_harmonic neg_neg zpow_natCast Rat.cast_pow Rat.cast_natCast Nat.cast_ofNat
padicValRat_two_harmonic 📖	mathematical	—	padicValRat harmonic Nat.log	—	padicValRat.zero Nat.log_zero_right Nat.cast_zero neg_zero eq_or_ne zero_add harmonic_succ Nat.cast_one inv_one padicValRat.one Nat.log_one_right padicValRat.inv Nat.fact_prime_two padicValRat.of_nat Int.instCharZero Nat.log_ne_padicValNat_succ padicValRat.add_eq_min LT.lt.ne' harmonic_pos inv_ne_zero Nat.cast_ne_zero Rat.instCharZero min_neg_neg Int.instIsOrderedAddMonoid Nat.cast_max Int.instIsStrictOrderedRing Nat.max_log_padicValNat_succ_eq_log_succ

---

← Back to Index