mul_scaleRoots_of_noZeroDivisors — Mathlib

English

In absence of zero divisors, the multiplicativity of scaleRoots holds: (p q).scaleRoots r = p.scaleRoots r · q.scaleRoots r.

Русский

При отсутствии делителей нуля множестенная совместимость scaleRoots: (p q).scaleRoots r = p.scaleRoots r · q.scaleRoots r.

LaTeX

$$$ (p q).\scaleRoots r = p.\scaleRoots r \cdot q.\scaleRoots r $$$

Lean4

theorem mul_scaleRoots_of_noZeroDivisors (p q : R[X]) (r : R) [NoZeroDivisors R] :
    (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r :=
  by
  by_cases hp : p = 0; · simp [hp]
  by_cases hq : q = 0; · simp [hq]
  apply mul_scaleRoots'
  simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero, hp, hq, or_self, not_false_eq_true]

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