factorization_le_factorization_of_dvd_right

English

For any a, and natural b,c with b | c and b,c ≠ 0, the p-adic exponent in b! is at most that in c!.

Русский

Для любого a и натуральных b,c с b|c и b≠0, c≠0 показатель p в b! не превышает показатель в c!.

LaTeX

$$$ b!\\!\\text{factorization }a \\le c!\\!\\text{factorization }a. $$$

Lean4

/-- Modified version of `emultiplicity_le_emultiplicity_of_dvd_right`
but for factorization. -/
theorem factorization_le_factorization_of_dvd_right (h : b ∣ c) (hb : b ≠ 0) (hc : c ≠ 0) :
    b.factorization a ≤ c.factorization a := by obtain ⟨k, rfl⟩ := h;
  simp [factorization_mul hb (Nat.ne_zero_of_mul_ne_zero_right hc)]

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