mem_nthRootsFinset — Mathlib

English

For 0 < n, x ∈ nthRootsFinset n a iff x^n = a

Русский

Для 0 < n верно: x принадлежит nthRootsFinset n a тогда и только тогда, когда x^n = a.

LaTeX

$$$0 < n \Rightarrow x \in \operatorname{nthRootsFinset}(n, a) \Leftrightarrow x^{n} = a$$$

Lean4

@[simp]
theorem mem_nthRootsFinset {n : ℕ} (h : 0 < n) (a : R) {x : R} : x ∈ nthRootsFinset n a ↔ x ^ (n : ℕ) = a := by
  classical rw [nthRootsFinset_def, mem_toFinset, mem_nthRoots h]

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