mathlib

f92fd0d1 - refactor(algebra/divisibility, associated): generalize instances in divisibility, associated (#3714)

refactor(algebra/divisibility, associated): generalize instances in divisibility, associated (#3714) generalizes the divisibility relation to noncommutative monoids adds missing headers to algebra/divisibility generalizes the instances in many of the lemmas in algebra/associated reunites (some of the) divisibility API for ordinals with general monoids Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>