Commit 2024-12-20 16:26 128a213e

feat(RingTheory): AlgebraicIndependent persists to algebraicClosure (#19708)

• AlgebraicIndependent.extendScalars: if A/S/R is a tower of algebras with S/R algebraic, then a family of elements in A that are algebraically independent over R remains algebraically independent over S, provided that S has no zero divisors.
• AlgebraicIndependent.algebraicClosure: an algebraically independent family remains algebraically independent over the algebraic closure. To prove these, we slightly change the statement of algebraicIndependent_of_finite(_type)' to keep a hypothesis inherited from Set.Finite.induction_on' to make induction work.