Theorem RingHom.IsIntegral.isLocalHom

Modification history

2025-08-09 19:57
Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
feat(RingTheory): integral extensions of comm. rings are local homs (#26746) …
Added RingHom.IsIntegral.isLocalHomView on Github →