UFDs, GCD domains and integrally closed domains in Mathlib

Stream: new members

[Isak Colboubrani]

I want to assert that ℚ is a.) an UFD, b.) a GCD domain and c.) an integrally closed domain.

This is my #mwe:

import Mathlib

-- Assert that ℚ is an unique factorization domain (UFD)
instance : UniqueFactorizationMonoid ℚ := by infer_instance
instance : IsDomain ℚ := by infer_instance

-- Assert that ℚ is a GCD domain
instance : GCDMonoid ℚ := by infer_instance
instance : IsDomain ℚ := by infer_instance

-- Assert that ℚ is an integrally closed domain
instance : IsIntegrallyClosed ℚ := by infer_instance
instance : IsDomain ℚ := by infer_instance

Do these assertions correspond correctly with the properties of ℚ as demonstrated by the code?

Is there anything that could be improved?

[Ruben Van de Velde]

Seems correct