Commit 2025-05-22 10:19 09b7c9b6

View on Github →

feat: Algebra.IsIntegral.of_surjective_algebraMap (#25066)

Estimated changes

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

added theorem Algebra.IsIntegral.of_surjective_algebraMap