Structures · Algebra

DivisibleBy

An AddMonoid A is α-divisible iff n • x = a has a solution for all n ≠ 0 ∈ α and a ∈ A. Here we adopt a constructive approach where we ask an explicit div : A → α → A function such that * div a 0 = 0 for all a ∈ A * n • div a n = a for all n ≠ 0 ∈ α and a ∈ A.

Defined in

Mathlib.GroupTheory.Divisible

Shape

2 explicit arguments · adds div, div_zero, div_cancel