Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-28 01:45 d8726bf3

View on Github →

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.

Estimated changes