Theorem algebraMap_isIntegral_iff

Modification history

2025-08-09 19:57
Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean
feat(RingTheory): integral extensions of comm. rings are local homs (#26746) …
Added algebraMap_isIntegral_iffView on Github →