Theorem Polynomial.Gal.mapRoots_bijective

Modification history

2025-11-20 19:42

Mathlib/FieldTheory/PolynomialGaloisGroup.lean

feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)

Modified Polynomial.Gal.mapRoots_bijective View on Github →

2023-06-23 10:52

Mathlib/FieldTheory/PolynomialGaloisGroup.lean

feat: port FieldTheory.PolynomialGaloisGroup (#5159)

Added Polynomial.Gal.mapRoots_bijective View on Github →