factorization_mul — Mathlib

English

For nonzero a,b, factorization(a b) = factorization(a) + factorization(b).

Русский

Для ненулевых a,b: factorization(a b) = factorization(a) + factorization(b).

LaTeX

$$$\\text{factorization}(a b) = \\text{factorization}(a) + \\text{factorization}(b)$$$

Lean4

/-- For nonzero `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
@[simp]
theorem factorization_mul {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) :
    factorization (a * b) = factorization a + factorization b := by simp [factorization, normalizedFactors_mul ha hb]

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