mathlib

41cf8de0 - feat(ring_theory/algebraic): `alg_hom` from an algebraic extension to itself is bijective (#15873)

feat(ring_theory/algebraic): `alg_hom` from an algebraic extension to itself is bijective (#15873) + Generalizes `alg_hom.bijective` and [alg_equiv_equiv_alg_hom](https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html#alg_equiv_equiv_alg_hom) and move them so that they can be derived from the generalized versions. Upgrade `alg_equiv_equiv_alg_hom` to a `mul_equiv` by introducing the monoid instance `alg_hom.End` on self-alg_homs. + Show that algebraicity of an algebra is preserved under alg_equiv (`alg_equiv.is_algebraic_iff`). [Zulip](https://leanprover.zulipchat.com/#narrow/stream/304774-FLT-regular/topic/Project.20status/near/292112817)