card_nthRoots — Mathlib

English

The cardinality of nthRoots(n,a) is at most n

Русский

Кардинал многосета nthRoots(n,a) не превосходит n.

LaTeX

$$$\operatorname{card}(\operatorname{nthRoots}(n, a)) \le n$$$

Lean4

theorem card_nthRoots (n : ℕ) (a : R) : Multiset.card (nthRoots n a) ≤ n := by
  classical
    exact
    (if hn : n = 0 then
      if h : (X : R[X]) ^ n - C a = 0 then by simp [nthRoots, roots, h, empty_eq_zero, Multiset.card_zero]
      else
        WithBot.coe_le_coe.1
          (le_trans (card_roots h)
            (by
              rw [hn, pow_zero, ← C_1, ← RingHom.map_sub]
              exact degree_C_le))
    else by
      rw [← Nat.cast_le (α := WithBot ℕ)]
      rw [← degree_X_pow_sub_C (Nat.pos_of_ne_zero hn) a]
      exact card_roots (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero hn) a))

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