Commit 2023-11-02 16:15 502bbf58
View on Github →feat: Galois orbits in a normal extension are determined by minimal polynomials (#8028)
Add Normal.minpoly_eq_iff_mem_orbit: addresses https://github.com/leanprover-community/mathlib4/pull/6718/files#r1328899532
Also generalize AlgHom.normal_bijective to Algebra.IsAlgebraic.bijective_of_isScalarTower' and golf the proof using a set-theoretic lemma Surjective.of_comp_left (slow to build, awaiting CI).