Commit 2024-07-17 12:28 d8041d9f

View on Github →

chore (Algebra.Basic): split results on Algebra's over Rat to a separate file (#14567) By putting dependencies on LinearOrderedField Rat in Algebra.Basic, we import too much unnecessary machinery and carry it downstream. This splits off the LinearOrderedField Rat declaration into Algebra.Algebra.Rat.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

deleted theorem RingHom.map_rat_algebraMap

deleted theorem algebraMap_rat_rat

Modified Mathlib/Algebra/Algebra/Hom.lean

deleted theorem AlgHom.toRingHom_toRatAlgHom

deleted def RingHom.equivRatAlgHom

deleted def RingHom.toRatAlgHom

deleted theorem RingHom.toRatAlgHom_toRingHom

Created Mathlib/Algebra/Algebra/Hom/Rat.lean

added theorem AlgHom.toRingHom_toRatAlgHom

added def RingHom.equivRatAlgHom

added def RingHom.toRatAlgHom

added theorem RingHom.toRatAlgHom_toRingHom

Created Mathlib/Algebra/Algebra/Rat.lean

added theorem RingHom.map_rat_algebraMap

added theorem algebraMap_rat_rat

Modified Mathlib/Algebra/Homology/ExactSequence.lean

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

Modified Mathlib/Algebra/TrivSqZeroExt.lean

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/Data/Complex/FiniteDimensional.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/Data/Real/Irrational.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

Modified Mathlib/NumberTheory/NumberField/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/RingTheory/PowerSeries/WellKnown.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

Created Mathlib/Topology/Algebra/Algebra/Rat.lean

Created test/instance_diamonds/Data/Complex/Module.lean

Created test/instance_diamonds/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Created test/instance_diamonds/FieldTheory/SplittingField/Construction.lean