Defs

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

Statistics

Metric	Count
Definitions	0
Theorems toNat_emultiplicity, le_emultiplicity_iff_replicate_subperm_primeFactorsList, le_padicValNat_iff_replicate_subperm_primeFactorsList, eq_zero_iff, maxPowDiv_eq_emultiplicity, maxPowDiv_eq_multiplicity, one, zero, padicValNat_def, padicValNat_def', padicValNat_eq_emultiplicity, padicValNat_eq_emultiplicity_of_ne_one	12
Total	12

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNat_emultiplicity 📖	mathematical	—	ENat.toNat emultiplicity instMonoid padicValNat	—	eq_or_ne emultiplicity_one_left padicValNat_one_left emultiplicity_zero padicValNat_zero_right

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_emultiplicity_iff_replicate_subperm_primeFactorsList 📖	mathematical	Nat.Prime	ENat instLEENat 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
padicValNat_def 📖	mathematical	—	padicValNat multiplicity Nat.instMonoid	—	padicValNat_def' Nat.Prime.ne_one Fact.out
padicValNat_def' 📖	mathematical	—	padicValNat multiplicity Nat.instMonoid	—	multiplicity_eq_of_emultiplicity_eq_some padicValNat_eq_emultiplicity_of_ne_one
padicValNat_eq_emultiplicity 📖	mathematical	—	ENat ENat.instNatCast padicValNat emultiplicity Nat.instMonoid	—	padicValNat_eq_emultiplicity_of_ne_one Nat.Prime.ne_one Fact.out
padicValNat_eq_emultiplicity_of_ne_one 📖	mathematical	—	ENat ENat.instNatCast padicValNat emultiplicity Nat.instMonoid	—	emultiplicity_eq_coe Nat.pow_dvd_iff_le_padicValNat instReflLe IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd

padicValNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_iff 📖	mathematical	—	padicValNat	—	eq_or_ne padicValNat_zero_right padicValNat_one_left Unique.instSubsingleton Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd pow_one Iff.not Nat.pow_dvd_iff_le_padicValNat
maxPowDiv_eq_emultiplicity 📖	mathematical	—	ENat ENat.instNatCast padicValNat emultiplicity Nat.instMonoid	—	padicValNat_eq_emultiplicity
maxPowDiv_eq_multiplicity 📖	mathematical	—	padicValNat multiplicity Nat.instMonoid	—	padicValNat_def'
one 📖	mathematical	—	padicValNat	—	padicValNat_one_right
zero 📖	mathematical	—	padicValNat	—	padicValNat_zero_right

---

← Back to Index