Commit 2023-11-03 09:34 bfdf7d09

View on Github →

chore: golf IsSplittingField.algEquiv (#8142) Also golfs Normal.of_algEquiv and Algebra.IsIntegral.of_finite and refactors Algebra.IsAlgebraic.bijective_of_isScalarTower.

Estimated changes

Modified Mathlib/FieldTheory/Normal.lean

modified theorem Normal.of_algEquiv

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

modified def Polynomial.IsSplittingField.algEquiv

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.Injective.bijective₂_of_surjective

modified theorem Function.Injective.of_comp_iff

added theorem Function.Surjective.bijective₂_of_injective

Modified Mathlib/RingTheory/Algebraic.lean

added theorem Algebra.IsAlgebraic.algHom_bijective₂

Modified Mathlib/RingTheory/IntegralClosure.lean

modified theorem Algebra.IsIntegral.of_finite