This commit is the last that is guaranteed to be synchronized with ma…

…thlib4

feat(measure_theory/constructions/polish): quotient group is a Borel …

…space (#19186)

* Suslin's theorem: an analytic set with analytic complement is measurable.
* Image of a measurable set in a Polish space under a measurable map is an analytic set.
* Preimage of a set under a measurable surjective map from a Polish
  space is measurable iff the original set is measurable.
* Quotient space of a Polish space with quotient σ-algebra is a Borel space provided that it has second countable topology.
* In particular, quotient group of a Polish topological group is a Borel space.
* Change instance for `measurable_space` on `add_circle`.

feat(data/equiv/algebra): automorphism groups for other structures (#…

…1141)

* Added automorphism groups to data/algebra/lean

* feat(data/equiv/algebra):
added automorphism groups

* feat(data/equiv/algebra)
Added automorphism groups

* Minor formatting

* feat(data/equiv/algebra):  add automorphism groups

* Changes based on comments

* minor change

* changes to namespaces and comments added

* expanding comments

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Added monoid case

* Changed Type to Type* also further up in the file

* typo

* I made it compile but not pretty

* More changes

* fixed typo

* fix universes

* update docs

* minor change

* use coercion rather than to_fun in ext lemmas

* Use ≃+* and coercion in ring_equiv.ext

* arguments of group.aut?

* generalize ring_equiv.ext to semirings

* Various changes

* Use only `mul_aut`, `add_aut`, and `ring_aut` for automorphisms.

* Make `*_equiv.ext` arguments agree with `equiv.ext`.

* Adjust documentation.

* Fix compile, add `add_aut.to_perm`