aroots_C_mul — Mathlib

English

If a ≠ 0, then (C(a) · p) has the same roots as p.

Русский

Если a ≠ 0, то (C(a) · p) имеет те же корни, что и p.

LaTeX

$$$$ (C(a)\cdot p)\aroots_S = p\aroots_S \quad (a \neq 0) $$$$

Lean4

@[simp]
theorem aroots_C_mul [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (p : T[X]) (ha : a ≠ 0) :
    (C a * p).aroots S = p.aroots S :=
  by
  rw [aroots_def, Polynomial.map_mul, map_C, roots_C_mul]
  rwa [map_ne_zero_iff]
  exact FaithfulSMul.algebraMap_injective T S

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