mathlib3

010bc64b - Fix `factorization_choose_of_lt_three_mul`