algebra/gcd_domain

Stream: general

[Johan Commelin]

Why are there all sorts of facts about int in this file? Shouldn't those go in some int/ directory? This file should be just about gcd_domains, right?
See everything from https://github.com/leanprover-community/mathlib/blob/master/src/algebra/gcd_domain.lean#L420 and onwards