Structures · Algebra

RootableBy

A Monoid A is α-rootable iff xⁿ = a has a solution for all n ≠ 0 ∈ α and a ∈ A. Here we adopt a constructive approach where we ask an explicit root : A → α → A function such that * root a 0 = 1 for all a ∈ A * (root a n)ⁿ = a for all n ≠ 0 ∈ α and a ∈ A.

Defined in

Mathlib.GroupTheory.Divisible

Shape

2 explicit arguments · adds root, root_zero, root_cancel