mathlib

65f8148b - chore(algebra/field_power): golf some proofs (#9170)