Zulip Chat Archive

Stream: new members

Topic: definition for GCD for ideals, fractional field


view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jan 29 2019 at 08:12):

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

view this post on Zulip 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