Commit 2025-08-09 19:57 20573c62

View on Github →

feat(RingTheory): integral extensions of comm. rings are local homs (#26746) migrated from #23684

Estimated changes

Modified Mathlib/Algebra/Field/Equiv.lean

Modified Mathlib/Algebra/Group/Invertible/Basic.lean

deleted def Units.invertible

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Proper.lean

Modified Mathlib/FieldTheory/LinearDisjoint.lean

Modified Mathlib/LinearAlgebra/Dimension/Localization.lean

Modified Mathlib/NumberTheory/RamificationInertia/Unramified.lean

Modified Mathlib/RingTheory/Artinian/Ring.lean

Modified Mathlib/RingTheory/Ideal/Int.lean

Modified Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean

added theorem algebraMap_isIntegral_iff

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

modified theorem Algebra.IsIntegral.isField_iff_isField

added theorem RingHom.IsIntegral.isLocalHom

modified theorem isField_of_isIntegral_of_isField

Modified Mathlib/RingTheory/LinearDisjoint.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/RingTheory/SimpleRing/Field.lean