definition for GCD for ideals, fractional field

Stream: new members

[Aditya Agarwal]

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]

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

[Aditya Agarwal]

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