Theorem Algebra.IsIntegral.of_surjective_algebraMap

Modification history

2025-05-23 11:00
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
chore(RingTheory/IntegralClosure): remove duplicate (#25120) …
Deleted Algebra.IsIntegral.of_surjective_algebraMapView on Github →
2025-05-22 10:19
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
feat: `Algebra.IsIntegral.of_surjective_algebraMap` (#25066)
Added Algebra.IsIntegral.of_surjective_algebraMapView on Github →