nthRootsFinset_toSet — Mathlib

English

For a domain R and n > 0, the finite set of nth roots equals { r ∈ R | r^n = a }. In particular, nthRootsFinset n a = { r | r^n = a } when 0 < n.

Русский

Для домена R и n > 0 множество корней степени n полагается ровно { r ∈ R | r^n = a }. В частности, nthRootsFinset n a = { r | r^n = a } при 0 < n.

LaTeX

$$$$ nthRootsFinset\, n\, a = \{ r \in R \mid r^n = a \} \quad\text{for } 0 < n $$$$

Lean4

@[simp]
theorem nthRootsFinset_toSet {n : ℕ} (h : 0 < n) (a : R) : nthRootsFinset n a = {r | r ^ n = a} :=
  by
  ext x
  simp_all

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