Commit 2022-08-11 16:08 41cf8de0

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 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