Commit 2024-11-23 04:58 506763e8

View on Github →

chore: rename *tower_top_of_injective lemmas (#19246)

Estimated changes

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/RingTheory/Algebraic.lean

added theorem Algebra.IsAlgebraic.extendScalars

deleted theorem Algebra.IsAlgebraic.tower_top_of_injective

added theorem IsAlgebraic.extendScalars

deleted theorem IsAlgebraic.tower_top_of_injective

deleted theorem Transcendental.of_tower_top_of_injective

added theorem Transcendental.restrictScalars

Modified Mathlib/RingTheory/AlgebraicIndependent.lean

Modified Mathlib/RingTheory/Localization/Integral.lean