mathlib3

084ba5e0 - feat({data/finset/basic, ring_theory/roots_of_unity, algebra/ring/units}): add lemmas (#17671)