Commit 2020-09-28 01:45 d8726bf3

feat(ring_theory/integral_closure): Explicitly define integral extensions (#4164)

• Defined ring_hom.is_integral_elem as a generalization of is_integral that takes a ring homomorphism rather than an algebra. The old version is is redefined to be (algebra_map R A).is_integral_elem x.
• Create predicates ring_hom.is_integral and algebra.is_integral representing when the entire extension is integral over the base ring.