Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-09-17 09:53
b755dda4
View on Github →
feat(RingTheory/IntegralClosure/IsIntegralClosure/Basic): add isIntegral_iff_of_equiv (
#15738
)
Estimated changes
Modified
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
added
theorem
mem_integralClosure_iff
Modified
Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
added
theorem
RingEquiv.isIntegral_iff