rootSet_monomial — Mathlib

English

If S is a field and an algebra over R, then the root set of the monomial a·X^n with a ≠ 0 is {0} (for n ≠ 0).

Русский

Если S — поле и есть алгебра над R, то корневой набор мононимиальной величины a·X^n (a ≠ 0, n ≠ 0) равен {0}.

LaTeX

$$$\bigl(\mathrm{monomial}\ n\ a\bigr).\mathrm{rootSet} S = \{0\}$$$

Lean4

theorem rootSet_monomial [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R} (ha : a ≠ 0) :
    (monomial n a).rootSet S = {0} := by
  classical
    rw [rootSet, aroots_monomial ha, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]

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