This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter.

This is extracted from #7907, which adds a more general nth root typeclass.
The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot.
This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does.

While perhaps claiming `√` for `Real.sqrt` is greedy; it:
* Is far more common thatn `NNReal.sqrt` and `Nat.sqrt`
* Is far more interesting to mathlib than `sqrt` on `Float`
* Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types.
* Will be replaced by a more general typeclass in a future PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter.

This is extracted from #7907, which adds a more general nth root typeclass.
The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot.
This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does.

While perhaps claiming `√` for `Real.sqrt` is greedy; it:
* Is far more common thatn `NNReal.sqrt` and `Nat.sqrt`
* Is far more interesting to mathlib than `sqrt` on `Float`
* Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types.
* Will be replaced by a more general typeclass in a future PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter.

This is extracted from #7907, which adds a more general nth root typeclass.
The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot.
This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does.

While perhaps claiming `√` for `Real.sqrt` is greedy; it:
* Is far more common thatn `NNReal.sqrt` and `Nat.sqrt`
* Is far more interesting to mathlib than `sqrt` on `Float`
* Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types.
* Will be replaced by a more general typeclass in a future PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter.

This is extracted from #7907, which adds a more general nth root typeclass.
The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot.
This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does.

While perhaps claiming `√` for `Real.sqrt` is greedy; it:
* Is far more common thatn `NNReal.sqrt` and `Nat.sqrt`
* Is far more interesting to mathlib than `sqrt` on `Float`
* Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types.
* Will be replaced by a more general typeclass in a future PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter.

This is extracted from #7907, which adds a more general nth root typeclass.
The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot.
This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does.

While perhaps claiming `√` for `Real.sqrt` is greedy; it:
* Is far more common thatn `NNReal.sqrt` and `Nat.sqrt`
* Is far more interesting to mathlib than `sqrt` on `Float`
* Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types.
* Will be replaced by a more general typeclass in a future PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter.

This is extracted from #7907, which adds a more general nth root typeclass.
The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot.
This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does.

While perhaps claiming `√` for `Real.sqrt` is greedy; it:
* Is far more common thatn `NNReal.sqrt` and `Nat.sqrt`
* Is far more interesting to mathlib than `sqrt` on `Float`
* Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types.
* Will be replaced by a more general typeclass in a future PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

This adds the notation `√r` for `Real.sqrt r`. The precedence is such that `√x⁻¹` is parsed as `√(x⁻¹)`; not because this is particularly desirable, but because it's the default and the choice doesn't really matter.

This is extracted from #7907, which adds a more general nth root typeclass.
The idea is to perform all the boring substitutions downstream quickly, so that we can play around with custom elaborators with a much slower rate of code-rot.
This PR also won't rot as quickly, as it does not forbid writing `x.sqrt` as that PR does.

While perhaps claiming `√` for `Real.sqrt` is greedy; it:
* Is far more common thatn `NNReal.sqrt` and `Nat.sqrt`
* Is far more interesting to mathlib than `sqrt` on `Float`
* Can be overloaded anyway, so this does not prevent downstream code using the notation on their own types.
* Will be replaced by a more general typeclass in a future PR.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502)



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>