## Stream: new members

### Topic: definition for GCD for ideals, fractional field

#### Aditya Agarwal (Jan 29 2019 at 03:54):

Is the fractional field for an arbitrary integral domain defined anywhere in mathlib?
I see that localization is defined, which I guess would be the way to define a fractional field if it isn't already present.

Also, is the ideal definition of GCD, i.e. gcd(I) = the smallest Principal Ideal containing I present in Lean?

#### Patrick Massot (Jan 29 2019 at 08:12):

https://github.com/leanprover/mathlib/blob/042c290dac25b5f1c77255f1039fae301774d6cf/src/ring_theory/localization.lean#L161

#### Aditya Agarwal (Jan 29 2019 at 08:15):

Thanks! Somehow I missed that one while grepping for quotient :upside_down:

Last updated: May 13 2021 at 06:15 UTC