mem_nthRoots — Mathlib

English

The Finset version of nthRoots simply collects the elements of nthRoots into a finite set (removing multiplicities).

Русский

Финсетная версия nthRootsSimply собирает элементы nthRoots в конечный набор, удаляя кратности.

LaTeX

$$$x \in \operatorname{nthRootsFinset}(n, a) \iff x \in \operatorname{nthRoots}(n, a)$$$

Lean4

@[simp]
theorem mem_nthRoots {n : ℕ} (hn : 0 < n) {a x : R} : x ∈ nthRoots n a ↔ x ^ n = a := by
  rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow, eval_X, sub_eq_zero]

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