mathlib

6152d450 - refactor(field_theory/perfect_closure): use bundled homs, review (#2357)

refactor(field_theory/perfect_closure): use bundled homs, review (#2357) * refactor(field_theory/perfect_closure): use bundled homs, review Also add lemmas like `monoid_hom.iterate_map_mul`. * Fix a typo spotted by `lint` * Apply suggestions from code review Co-Authored-By: Johan Commelin <johan@commelin.net> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>