This PR protects `Function.Commute`, so that it no longer clashes with `Commute` in the root namespace, as suggested by @j-loreaux in #6290.

… ≃ (Aᵐᵒᵖ ≃ₐ[R] B)` (#6525)

This also adds the missing `AlgEquiv.equivCongr` as a more general version of `AlgEquiv.autCongr`.

…ar order (#6571)

Currently, in a conditionally complete linear order, the supremum of an unbounded set hasn't any specific property. However, in all instances in mathlib, all unbounded sets have the same supremum. This PR adds this requirement in mathlib. This will be convenient to remove boundedness assumptions in measurability statements.

The main changes are:

- we replace the data-bearing `PerfectRing` typeclass with a `Prop`-valued (non-constructive) version,
- we introduce a new typeclass `PerfectField`,
- we add a proof that a perfect field of positive characteristic has surjective Frobenius map,
- we add some basic facts such as perfection of finite rings / fields and products of perfect rings.

Removing some linters and error codes that are not Lean 4 relevant



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…⊗[R] B)ᵐᵒᵖ` (#6555)

Prove [Gershgorin circle theorem](https://en.wikipedia.org/wiki/Gershgorin_circle_theorem) and some applications that will be useful for the proof of Dirichlet's unit theorem #5960

… identities (#6139)

Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>
Co-authored-by: Oliver Nash <github@olivernash.org>

Co-authored-by: Patrick Massot <patrickmassot@free.fr>

…y/mathlib4 into edit_distance_bounds