factorization_eq_card_pow_dvd_of_lt

English

If a and b are coprime and p is a prime factor of a, then the exponent of p in a b equals the exponent of p in a.

Русский

Если a и b взаимно просты и p — простой делитель a, то показатель p в ab равен показателю p в a.

LaTeX

$$$ (a \cdot b).factorization p = a.factorization p \quad$ при $\gcd(a,b)=1$ и $p \in a.primeFactorsList$$$

Lean4

/-- The factorization of `m` in `n` is the number of positive natural numbers `i` such that `m ^ i`
divides `n`. Note `m` is prime. This set is expressed by filtering `Ico 1 b` where `b` is any bound
greater than `log m n`. -/
theorem factorization_eq_card_pow_dvd_of_lt (hm : m.Prime) (hn : 0 < n) (hb : n < m ^ b) :
    n.factorization m = #({i ∈ Ico 1 b | m ^ i ∣ n}) := by
  rwa [factorization_eq_card_pow_dvd n hm, Ico_pow_dvd_eq_Ico_of_lt hm (by cutsat)]

Похожие утверждения