Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-16 19:04 38d5c120

View on Github →

feat(ring_theory/integral_closure): integral closure (#1087)

feat(ring_theory/integral_closure): integral closure
update

Estimated changes

Created src/ring_theory/integral_closure.lean

added theorem fg_adjoin_of_finite

added theorem fg_adjoin_singleton_of_integral

added def integral_closure

added theorem integral_closure_idem

added def is_integral

added theorem is_integral_add

added theorem is_integral_algebra_map

added theorem is_integral_iff_is_integral_closure_finite

added theorem is_integral_mul

added theorem is_integral_neg

added theorem is_integral_of_mem_closure

added theorem is_integral_of_mem_of_fg

added theorem is_integral_of_noetherian'

added theorem is_integral_of_noetherian

added theorem is_integral_of_subring

added theorem is_integral_one

added theorem is_integral_sub

added theorem is_integral_zero

added theorem mem_integral_closure_iff_mem_fg