mathlib3

a4f6c41e - move(algebra/field_power): Put lemmas in the correct place (#16465)

move(algebra/field_power): Put lemmas in the correct place (#16465) `algebra.field_power` is only made of lemmas that belong elsewhere. Move them and delete the file. Golf proofs while we're at it and make `min_le_of_zpow_le_max` an iff.