Square root typeclass

Stream: mathlib4

[Violeta Hernández]

There's a TODO comment above the docs#Real.sqrt notation, suggesting turning it into a typeclass. Has there been any progress on this?

[Yakov Pechersky]

src#Real.sqrt

[Kevin Buzzard]

What does this comment even mean? Edit: oh, the issue seems to be that the notation should be HasSqrt.sqrt so it works for NNReal etc.

[Violeta Hernández]

I imagine it means one of two things

• Make a typeclass for the notation
• Make a typeclass for types with a "well-behaved" square root operation

[Violeta Hernández]

I'm not sure what the second one would entail (and I don't really find it feasible), but the first one seems very uncontroversial

[Niels Voss]

Do we want to turn Nat.sqrt into a typeclass instance? I personally don't think that's a good idea, but I want to hear what other people's perspectives are

[Violeta Hernández]

I don't really see why not. It might look a bit weird to write stuff like √5 = 2 but I'd argue this is no worse than what Nat substraction and division already allow.

[Niels Voss]

I guess that's fair. I'm just used to having sqrt automatically coerce Nat to Real

[Violeta Hernández]

Hmmm yeah, that's actually a really good point against this idea