Defs

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

Statistics

Metric	Count
Definitions padicValNat	1
Theorems le_emultiplicity_iff_replicate_subperm_primeFactorsList, le_padicValNat_iff_replicate_subperm_primeFactorsList, eq_zero_iff, one, zero, padicValNat_def, padicValNat_def', padicValNat_eq_emultiplicity	8
Total	9

(root)

Definitions

Name	Category	Theorems
padicValNat 📖	CompOp	61 math math: padicValNat.padicValNat_eq_maxPowDiv, padicValNat_add_le_self, pow_succ_padicValNat_not_dvd, Nat.max_log_padicValNat_succ_eq_log_succ, padicValNat.eq_zero_iff, sub_one_mul_padicValNat_factorial, padicValNat.pow_two_sub_one_ge, sub_one_mul_padicValNat_choose_eq_sub_sum_digits, padicValNat_dvd_iff, padicValNat.one, padicValNat_mul_div_factorial, padicValNat_prime_prime_pow, sub_one_mul_padicValNat_choose_eq_sub_sum_digits', padicValNat.zero, one_le_padicValNat_of_dvd, padicValNat.pow_sub_pow, padicValNat.pow, padicValNat_choose', Nat.eq_sq_add_sq_iff, Padic.valuation_ofNat, Nat.prod_pow_prime_padicValNat, padicValNat.pow_add_pow, padicValNat_factorial_le, padicValNat_def, padicValNat.self, padicValNat_self, sub_one_mul_padicValNat_factorial_lt_of_ne_zero, padicValNat.prime_pow, pow_padicValNat_dvd, le_padicValNat_iff_replicate_subperm_primeFactorsList, padicValNat_primes, padicValNat_choose, padicValNat_factorial, padicValNat.div_of_dvd, Nat.eq_iff_prime_padicValNat_eq, padicValNat.div_pow, padicValRat_def, padicValNat_def', padicValRat.of_nat, padicValNat.mul, nat_log_eq_padicValNat_iff, padicValNat.pow_two_sub_pow, padicValNat_factorial_lt_of_ne_zero, padicValInt.of_nat, Nat.factorization_def, padicValRat_of_nat, padicValNat.eq_zero_of_not_dvd, padicValNat.div', padicValNat_mul_pow_left, Padic.valuation_natCast, padicValNat.pow_two_sub_one, padicValNat_dvd_iff_le, padicValNat_eq_zero_of_mem_Ioo, range_pow_padicValNat_subset_divisors', padicValNat_factorial_mul_add, padicValNat.div, padicValNat_factorial_mul, padicValNat_mul_pow_right, range_pow_padicValNat_subset_divisors, padicValNat_le_nat_log, padicValNat_eq_emultiplicity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_emultiplicity_iff_replicate_subperm_primeFactorsList 📖	mathematical	Nat.Prime	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat ENat.instNatCast emultiplicity Nat.instMonoid Nat.primeFactorsList	—	Nat.replicate_subperm_primeFactorsList_iff pow_dvd_iff_le_emultiplicity
le_padicValNat_iff_replicate_subperm_primeFactorsList 📖	mathematical	Nat.Prime	padicValNat Nat.primeFactorsList	—	le_emultiplicity_iff_replicate_subperm_primeFactorsList FiniteMultiplicity.emultiplicity_eq_multiplicity Nat.finiteMultiplicity_iff Nat.Prime.ne_one padicValNat_def' Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
padicValNat_def 📖	mathematical	—	padicValNat multiplicity Nat.instMonoid	—	padicValNat_def' Nat.Prime.ne_one Fact.out
padicValNat_def' 📖	mathematical	—	padicValNat multiplicity Nat.instMonoid	—	Nat.finiteMultiplicity_iff Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable WithTop.untopD_coe
padicValNat_eq_emultiplicity 📖	mathematical	—	ENat ENat.instNatCast padicValNat emultiplicity Nat.instMonoid	—	FiniteMultiplicity.emultiplicity_eq_multiplicity Nat.finiteMultiplicity_iff Nat.Prime.ne_one Fact.out padicValNat_def

padicValNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_iff 📖	mathematical	—	padicValNat	—	Nat.instCanonicallyOrderedAdd zero_add pow_one
one 📖	mathematical	—	padicValNat	—	Nat.instZeroLEOneClass Nat.instIsMulTorsionFree Nat.find.congr_simp
zero 📖	mathematical	—	padicValNat	—	—

---

← Back to Index