Theorem RingHom.isIntegral_of_isIntegral_mul_unit

Modification history

2023-11-17 13:15
Mathlib/RingTheory/IntegralClosure.lean
chore(IntegralClosure): noncommutative generalizations and golfs (#8406) …
Deleted RingHom.isIntegral_of_isIntegral_mul_unitView on Github →
2023-07-04 05:50
Mathlib/RingTheory/IntegralClosure.lean
feat: port RingTheory.Jacobson (#4338)
Added RingHom.isIntegral_of_isIntegral_mul_unitView on Github →