Theorem Algebra.ker_algebraMap_isMaximal_of_isIntegral

Modification history

2026-03-26 00:06
Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
feat(RingTheory): adds lemmas/instances related to integral maps to a field and residue fields (#36790) …
Added Algebra.ker_algebraMap_isMaximal_of_isIntegralView on Github →