Theorem RingHom.isIntegral_respectsIso

Modification history

2023-06-13 10:21
Mathlib/RingTheory/RingHom/Integral.lean
feat: port RingTheory.RingHom.Integral (#5004)
Added RingHom.isIntegral_respectsIsoView on Github →