Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 05:50 b5eb0429

View on Github →

feat(ring_theory/integral_closure): finite = integral + finite_type (#15970)

Estimated changes

Modified src/ring_theory/finiteness.lean

added theorem ring_hom.finite_type.of_finite

Modified src/ring_theory/integral_closure.lean

added theorem algebra.finite_iff_is_integral_and_finite_type

added theorem algebra.is_integral.finite

added theorem algebra.is_integral.of_finite

added theorem ring_hom.finite.to_is_integral

added theorem ring_hom.finite_iff_is_integral_and_finite_type

added theorem ring_hom.is_integral.to_finite