MaxPowDiv

📁 Source: Mathlib/Data/Nat/MaxPowDiv.lean

Statistics

Metric	Count
Definitions maxPowDiv, go	2
Theorems base_mul_eq_succ, base_pow_mul, go_succ, le_of_dvd, pow_dvd, zero, zero_base	7
Total	9

Nat

Definitions

Name	Category	Theorems
maxPowDiv 📖	CompOp	9 math math: padicValNat.padicValNat_eq_maxPowDiv, padicValNat.maxPowDiv_eq_multiplicity, maxPowDiv.zero_base, maxPowDiv.le_of_dvd, maxPowDiv.pow_dvd, maxPowDiv.zero, maxPowDiv.base_mul_eq_succ, maxPowDiv.base_pow_mul, padicValNat.maxPowDiv_eq_emultiplicity

Nat.maxPowDiv

Definitions

Name	Category	Theorems
go 📖	CompOp	1 math math: go_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_mul_eq_succ 📖	mathematical	—	Nat.maxPowDiv	—	lt_trans Nat.instZeroLEOneClass go.eq_1 go_succ
base_pow_mul 📖	mathematical	—	Nat.maxPowDiv Monoid.toNatPow Nat.instMonoid	—	pow_zero one_mul add_zero mul_assoc mul_comm base_mul_eq_succ pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass pos_of_gt Nat.instCanonicallyOrderedAdd
go_succ 📖	mathematical	—	go	—	go.induct_unfolding go.eq_def
le_of_dvd 📖	mathematical	Monoid.toNatPow Nat.instMonoid	Nat.maxPowDiv	—	MulZeroClass.mul_zero base_pow_mul covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
pow_dvd 📖	mathematical	—	Monoid.toNatPow Nat.instMonoid Nat.maxPowDiv	—	go.eq_1 go_succ pow_succ zero_add pow_zero
zero 📖	mathematical	—	Nat.maxPowDiv	—	go.eq_1
zero_base 📖	mathematical	—	Nat.maxPowDiv	—	go.eq_1 Nat.instCanonicallyOrderedAdd

---

← Back to Index