Commit 2025-02-11 17:21 d1845dbb

View on Github →

chore(RingTheory/Algebraic): remove unnecessary injectivity assumptions (#21566) Also

Polynomial.exists_dvd_map_of_isAlgebraic is added as an application.
An easy instance Algebra.IsPushout R R[X] S S[X] is also added.
Prove Algebra.IsAlgebraic.injective_tower_top to remove injectivity assumption from AlgebraicIndependent.extendScalars.
Make the arguments of Algebra.IsAlgebraic.trans explicit.

Estimated changes

Modified Mathlib/FieldTheory/AlgebraicClosure.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

modified theorem IsAlgClosure.ofAlgebraic

Modified Mathlib/FieldTheory/PurelyInseparable/Basic.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem Polynomial.exists_dvd_map_of_isAlgebraic

Modified Mathlib/RingTheory/Algebraic/Basic.lean

added theorem Algebra.IsAlgebraic.faithfulSMul_tower_top

added theorem Algebra.IsAlgebraic.injective_tower_top

Modified Mathlib/RingTheory/Algebraic/Integral.lean

deleted theorem Algebra.IsAlgebraic.trans'

added theorem Algebra.IsAlgebraic.trans

modified theorem IsAlgebraic.exists_integral_multiple

modified theorem IsAlgebraic.iff_exists_smul_integral

modified theorem IsAlgebraic.of_finite

modified theorem Transcendental.extendScalars

modified theorem Transcendental.extendScalars_of_isIntegral

Modified Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean

modified theorem AlgebraicIndependent.extendScalars

modified theorem AlgebraicIndependent.extendScalars_of_isIntegral

deleted theorem AlgebraicIndependent.extendScalars_of_isSimpleRing

deleted theorem AlgebraicIndependent.subalgebra_of_isIntegral

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

modified def Polynomial.algebra