English
For certain m ≠ 1, n > 0 and bound b with log m n < b, the multiplicity emultiplicity m n equals the cardinality of {i ∈ Ico 1 b | m^i ∣ n}.
Русский
При некоторых m ≠ 1, n > 0 и ограничении b с log_m n < b кратность emultiplicity m n равна кардинальности множества {i ∈ Ico 1 b | m^i делится на n}.
LaTeX
$$$ emultiplicity(m,n) = \#\{ i \in Ico(1,b) \mid m^i \mid n \} \quad \text{при } m \neq 1,\ n > 0,\ log\ m\ n < b $$$
Lean4
/-- The multiplicity of `m` in `n` is the number of positive natural numbers `i` such that `m ^ i`
divides `n`. This set is expressed by filtering `Ico 1 b` where `b` is any bound greater than
`log m n`. -/
theorem emultiplicity_eq_card_pow_dvd {m n b : ℕ} (hm : m ≠ 1) (hn : 0 < n) (hb : log m n < b) :
emultiplicity m n = #({i ∈ Ico 1 b | m ^ i ∣ n}) :=
have fin := Nat.finiteMultiplicity_iff.2 ⟨hm, hn⟩
calc
emultiplicity m n = #(Ico 1 <| multiplicity m n + 1) := by simp [fin.emultiplicity_eq_multiplicity]
_ = #({i ∈ Ico 1 b | m ^ i ∣ n}) :=
congr_arg _ <|
congr_arg card <|
Finset.ext fun i =>
by
simp only [mem_Ico, Nat.lt_succ_iff, fin.pow_dvd_iff_le_multiplicity, mem_filter, and_assoc,
and_congr_right_iff, iff_and_self]
intro hi h
rw [← fin.pow_dvd_iff_le_multiplicity] at h
rcases m with - | m
· rw [zero_pow, zero_dvd_iff] at h
exacts [(hn.ne' h).elim, one_le_iff_ne_zero.1 hi]
refine LE.le.trans_lt ?_ hb
exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩) (le_of_dvd hn h)
