Mathlib v3 is deprecated. Go to Mathlib v4

Theorem unique_factorization_monoid.integrally_closed

Modification history

2021-08-27 17:22
src/ring_theory/polynomial/rational_root.lean
feat(ring_theory): define integrally closed domains (#8893) …
Deleted unique_factorization_monoid.integrally_closedView on Github →
2021-07-05 14:14
src/ring_theory/polynomial/rational_root.lean
refactor(ring_theory): turn `localization_map` into a typeclass (#8119) …
Modified unique_factorization_monoid.integrally_closedView on Github →
2020-09-22 06:16
src/ring_theory/polynomial/rational_root.lean
refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` (#4156) …
Added unique_factorization_monoid.integrally_closedView on Github →