Commit 2024-02-06 21:44 ec4beba2

View on Github →

refactor(FieldTheory/PerfectClosure): change the order of some results (#10282)

  • Now the perfect closure is a perfect ring without requiring base ring to be a field.
  • Add mk_pow and mk_surjective.
  • Add explicit names to all of the instances.
  • Add docstrings for the file.

Estimated changes

deleted theorem PerfectClosure.eq_iff'
added theorem PerfectClosure.mk_pow