mathlib3

f37aeb00 - refactor(algebra/gcd_monoid): drop nontriviality assumptions (#9568)