aroots_monomial — Mathlib

English

The roots of monomial n a are 0 with multiplicity n, for a ≠ 0.

Русский

Корни мономиала monomial n a — это 0 с кратностью n, если a ≠ 0.

LaTeX

$$$$ (\mathrm{monomial}\; n\; a)\aroots_S = n \cdot \{0\} \quad (a \neq 0) $$$$

Lean4

@[simp]
theorem aroots_monomial [CommRing S] [IsDomain S] [Algebra T S] [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0) (n : ℕ) :
    (monomial n a).aroots S = n • ({0} : Multiset S) := by rw [← C_mul_X_pow_eq_monomial, aroots_C_mul_X_pow ha]

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