nthRootsFinset — Mathlib

English

The Finset version is the Finset of nthRoots

Русский

Финсетная версия является конечным множеством из nthRoots.

LaTeX

$$$\operatorname{nthRootsFinset}(n, a) = (\operatorname{nthRoots}(n, a)).toFinset$$$

Lean4

/-- The multiset `nthRoots ↑n a` as a Finset. Previously `nthRootsFinset n` was defined to be
`nthRoots n (1 : R)` as a Finset. That situation can be recovered by setting `a` to be `(1 : R)` -/
def nthRootsFinset (n : ℕ) {R : Type*} (a : R) [CommRing R] [IsDomain R] : Finset R :=
  haveI := Classical.decEq R
  Multiset.toFinset (nthRoots n a)

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