Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_localization.surj_of_gcd_domain

Modification history

2022-07-16 11:29
src/algebra/gcd_monoid/integrally_closed.lean
feat(algebra/gcd_monoid): GCD domains are integrally closed. (#15109)
Added is_localization.surj_of_gcd_domainView on Github →