Stream: new members
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):
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