Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-11 16:08 41cf8de0

View on Github →

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

Estimated changes