Abbreviation for square root

[Norman Megill]

(Per AV's suggestion I started a new thread.)
Continuing: https://groups.google.com/d/msg/metamath/XPYuatviNV0/ziS-CsG-DQAJ

On Saturday, January 4, 2020 at 10:19:17 AM UTC-5, David A. Wheeler wrote:

Norman Megill:
>Our current square and square root conventions are "sq" and "sqr" resp.
>I'm almost certain I've seen "sqr" used for square root in at least one
>computer language although I can't recall which one right now.

I recall it now:  sqr for square root is used in BASIC and essentially all its derivatives (Visual BASIC, BASIC-Plus, etc.).  I think all of the standard arithmetic/trig functions (sqr, sin, cos, tan, atn,...) used 3 letters, so at least there was that small point of consistency that made them slightly easier to remember.  So historically I'm pretty sure I subconsciously chose that convention when adding the first square root theorems.  I don't recall ever seeing sqr used for square, probably because most languages use "^" or similar for powers.

[I was forced to use BASIC-Plus on a DEC VAX for several years because any other language at that time would have required the purchase of an exorbitantly expensive compiler that couldn't be justified.  Thankfully in the early 90s gcc became available for free.

At least BASIC-Plus had a "structured" extended language with "if...end" blocks etc, and no one used line numbers any more, so it wasn't terrible to program in.  It did require the first line of code to begin with a line number - usually people used 1 or 10 - and there were arguments among developers about why the lone line number needed to be retained.]

Norm
 

 I don't
>see
>the problem with omitting the "t" since any confusion is instantly
>resolved
>by hovering over the label, if the content of the proof step doesn't
>make
>it obvious.  If people are truly confused by this, I suppose we can add
>the
>"t", but until now no one has complained about it.

I am fine with sq as square, but square root is almost universally notated as sqrt.

Here is a list of just some of the languages that use sqrt for square root:
Fortran
C
Python
Excel
Java
C#
JavaScript
Common Lisp
Scheme
Mathematica
Octave / Matlab

In short, the standard abbreviation for square root is sqrt. We would make others' lives simpler by using the same abbreviation everyone else does.

[Alexander van der Vekens]

I am happy with sqr (I do not associate the "r" in sqr with the "r" in "square", but with the "r" in "root"), but I would also accept if it is changed to sqrt.

In any case, "sqr" or "sqrt" should be added to the table of abbreviations in subsection "17.1.1  Conventions".

Alexander

[Benoit]

Indeed, I think that BASIC also uses "sqr" for "square root", but for most modern languages, this is "sqrt". Anyway, "sqr" is indeed ambiguous, so I would prefer that in all labels, "sqr" be replaced with "sqrt".

Another, more important, change within labels would be to replace everywhere "rng" with "ring".  Indeed, "rng" might refer to "rngs", which is a common name for non-unital rings (rings that lost the "i" of "identity"). Therefore, it is ambiguous, and it might be more difficult than in the "sqr" case to deduce from a simple inspection if the given theorem refers to rngs or rings.

Indeed, the most important is to be consistent with conventions, and this is why I replaced recently, for instance:

imp3a --> impd

exp3a --> expd

con3and --> con3dimp

ee10 --> mpisyl
ee12an --> syl6an

a5d --> ax5d (and friends)

mpto1 --> mptnan
mpto2 --> mptxor
mtp-or --> mtpor
mtp-xor --> mtpxor

changed math token from "om" to "_om"

changed math token from "pi" to "_pi"
changed math token from "tau" to "_tau"

Benoît

[Alexander van der Vekens]

Hi Benoît

On Sunday, January 5, 2020 at 8:21:26 PM UTC+1, Benoit wrote:

Indeed, I think that BASIC also uses "sqr" for "square root", but for most modern languages, this is "sqrt". Anyway, "sqr" is indeed ambiguous, so I would prefer that in all labels, "sqr" be replaced with "sqrt".

Another, more important, change within labels would be to replace everywhere "rng" with "ring".  Indeed, "rng" might refer to "rngs", which is a common name for non-unital rings (rings that lost the "i" of "identity"). Therefore, it is ambiguous, and it might be more difficult than in the "sqr" case to deduce from a simple inspection if the given theorem refers to rngs or rings.

In principle, I agree with your suggestion to replace "rng" by "ring" for theorems about unital rings (and `Ring` is unital in set.mm). There are about 140 labels of theorems (in Parts 10-16 - only these should be relevant) containing "rng", and I think most of them should be renamed according to your proposal. In June 2019, I replaced already some labels (in the context of introducing ZZring) on your advise. On the other hand, there were changes of labels, replacing "ring" by "rng" for relevant labels, in 2013/14. There must have been a reason for this. Especially the label for the definition of a (unital) Ring, df-rng, was changed from df-ring to df-rng (see also https://groups.google.com/d/msg/metamath/HDQXr196Yo0/KhDrxgnRBgAJ) in July 2017, which should be reverted. But the table of abbreviations contains "rng" as convention to be used for (unital!) rings...

To continue the discussion, a separate thread should be opened for this topic (wasn't there a corresponding issue in GitHub?)!

Alexander

PS: Your recent changes of labels, especially impd and expd, are very helpful for me!

[Norman Megill]

On Sunday, January 5, 2020 at 4:22:13 PM UTC-5, Alexander van der Vekens wrote:

Hi Benoît

On Sunday, January 5, 2020 at 8:21:26 PM UTC+1, Benoit wrote:

Indeed, I think that BASIC also uses "sqr" for "square root", but for most modern languages, this is "sqrt". Anyway, "sqr" is indeed ambiguous, so I would prefer that in all labels, "sqr" be replaced with "sqrt".

Many acronyms we use in label parts are often ambiguous out of context in order to serve as short hints, with the understanding that the description or the theorem itself will provide clarification.  The goal isn't to reproduce computer languages.  For example, we use "itg" instead of "Integrate" like Mathematica.  The majority of our acronyms for parts of labels are 3 or less characters.  We have 30K labels built up from short parts, whereas computer languages have the luxury of just a few dozen functions that they can represent using single words or acronyms.  For example, they use "sqrt" as the entire label for a single function, whereas for us "sqr" is just one piece of maybe about 150 compound labels.

I'm still not completely sold on the idea that people find "sqr" ambiguous.  While BASIC and its dialects may be ugly from a modern computer science point of view, nonetheless it has been and maybe still is one of the most popular languages for beginners.  Probably millions of people have written programs in various dialects of BASIC without this confusion.  Is there any computer language anywhere that uses "sqr" for square?
 

Another, more important, change within labels would be to replace everywhere "rng" with "ring".  Indeed, "rng" might refer to "rngs", which is a common name for non-unital rings (rings that lost the "i" of "identity"). Therefore, it is ambiguous, and it might be more difficult than in the "sqr" case to deduce from a simple inspection if the given theorem refers to rngs or rings.

In principle, I agree with your suggestion to replace "rng" by "ring" for theorems about unital rings (and `Ring` is unital in set.mm). There are about 140 labels of theorems (in Parts 10-16 - only these should be relevant) containing "rng", and I think most of them should be renamed according to your proposal. In June 2019, I replaced already some labels (in the context of introducing ZZring) on your advise. On the other hand, there were changes of labels, replacing "ring" by "rng" for relevant labels, in 2013/14. There must have been a reason for this.

The reason was simply to be more consistent.  We only had one type of ring, and some places used "ring" while others used "rng".  I changed them to "rng", picking the shorter of the two choices.  I didn't know about the two spellings used in the literature for different kinds of rings.
 

Especially the label for the definition of a (unital) Ring, df-rng, was changed from df-ring to df-rng (see also https://groups.google.com/d/msg/metamath/HDQXr196Yo0/KhDrxgnRBgAJ) in July 2017, which should be reverted. But the table of abbreviations contains "rng" as convention to be used for (unital!) rings...

To continue the discussion, a separate thread should be opened for this topic (wasn't there a corresponding issue in GitHub?)!

I'm fine with making these changes since there is an ambiguity to be resolved, and it is good to conform somewhat more closely to math texts when it is practical to do so.  If no one else has an objection, I don't think we need to open a separate thread.  If you (BJ) want to create a PR for this when you find it convenient, please do so and we will accept it.
 

Alexander

PS: Your recent changes of labels, especially impd and expd, are very helpful for me!

I agree.

Norm

[Benoit]

Is there any computer language anywhere that uses "sqr" for square?

Pascal is one of them: http://xoomer.virgilio.it/gciabu/engl/pascal/pas038.htm

I understand the size concern with all the compound labels, but here it's only one letter, and related theorems are probably not used that much.

 

The reason was simply to be more consistent.  We only had one type of ring, and some places used "ring" while others used "rng".  I changed them to "rng", picking the shorter of the two choices.  I didn't know about the two spellings used in the literature for different kinds of rings.

I'm fine with making these changes since there is an ambiguity to be resolved, and it is good to conform somewhat more closely to math texts when it is practical to do so.  If no one else has an objection, I don't think we need to open a separate thread.  If you (BJ) want to create a PR for this when you find it convenient, please do so and we will accept it.

I'll wait for other potential objections (and for a period with more free time), and I'll try to create a PR soon...ish.

Benoît

[Norman Megill]

On Sunday, January 5, 2020 at 7:39:14 PM UTC-5, Benoit wrote:

Is there any computer language anywhere that uses "sqr" for square?

Pascal is one of them: http://xoomer.virgilio.it/gciabu/engl/pascal/pas038.htm

I understand the size concern with all the compound labels, but here it's only one letter, and related theorems are probably not used that much.

OK. you (or David or whoever wants) can add the "t".

Norm

[Norman Megill]

Note that 'sqr' occurs in mmset.raw.html, mm_100.html, index.html, mmhil.html, mmmusic.html, and symbols.html, so they will need to be updated at the same time.

Norm

[David A. Wheeler]

On Sun, 5 Jan 2020 16:52:07 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> OK. you (or David or whoever wants) can add the "t".

Okay. I did a quick look to see how many labels would probably change, by running this:
metamath 'read set.mm' 'set scroll continuous' 'set width 9999' 'show statement *sqr*' quit | grep ' sqr ' > ,sqr

It looks like it's less than 100. I think we can first change all the labels (e.g., "df-sqr" becomes "df-sqrt"), as listed below. We can then separately change the actual expressions so "sqr" becomes "sqrt". Doing this in separate steps should reduce the risk of errors in it.

--- David A. Wheeler

=========================================

40921 csqr $a class sqr $.
40925 df-sqr $a |- sqr = ( x e. CC |-> ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) ) $.
40927 sqrval $p |- ( A e. CC -> ( sqr ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) ) $= ... $.
40933 sqr0 $p |- ( sqr ` 0 ) = 0 $= ... $.
40967 resqrcl $p |- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR ) $= ... $.
40968 resqrthlem $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqr ` A ) ) /\ ( _i x. ( sqr ` A ) ) e/ RR+ ) ) $= ... $.
40970 resqrth $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) ^ 2 ) = A ) $= ... $.
40971 remsqsqr $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A ) $= ... $.
40972 sqrge0 $p |- ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( sqr ` A ) ) $= ... $.
40973 sqrgt0 $p |- ( ( A e. RR /\ 0 < A ) -> 0 < ( sqr ` A ) ) $= ... $.
40974 sqrmul $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) ) $= ... $.
40975 sqrle $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) ) $= ... $.
40976 sqrlt $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) ) $= ... $.
40977 sqr11 $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) = ( sqr ` B ) <-> A = B ) ) $= ... $.
40978 sqr00 $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) = 0 <-> A = 0 ) ) $= ... $.
40979 rpsqrcl $p |- ( A e. RR+ -> ( sqr ` A ) e. RR+ ) $= ... $.
40980 sqrdiv $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) ) $= ... $.
40981 sqrneglem $p |- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( _i x. ( sqr ` A ) ) ^ 2 ) = -u A /\ 0 <_ ( Re ` ( _i x. ( sqr ` A ) ) ) /\ ( _i x. ( _i x. ( sqr ` A ) ) ) e/ RR+ ) ) $= ... $.
40984 sqrneg $p |- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` -u A ) = ( _i x. ( sqr ` A ) ) ) $= ... $.
40986 sqrsq2 $p |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) ) $= ... $.
40987 sqrsq $p |- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` ( A ^ 2 ) ) = A ) $= ... $.
40988 sqrmsq $p |- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` ( A x. A ) ) = A ) $= ... $.
40989 sqr1 $p |- ( sqr ` 1 ) = 1 $= ... $.
40990 sqr4 $p |- ( sqr ` 4 ) = 2 $= ... $.
40991 sqr9 $p |- ( sqr ` 9 ) = 3 $= ... $.
40992 sqr2gt1lt2 $p |- ( 1 < ( sqr ` 2 ) /\ ( sqr ` 2 ) < 2 ) $= ... $.
40993 sqrm1 $p |- _i = ( sqr ` -u 1 ) $= ... $.
41151 sqreulem.1 $e |- B = ( ( sqr ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) ) $.
41160 sqrcl $p |- ( A e. CC -> ( sqr ` A ) e. CC ) $= ... $.
41161 sqrthlem $p |- ( A e. CC -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqr ` A ) ) /\ ( _i x. ( sqr ` A ) ) e/ RR+ ) ) $= ... $.
41162 sqrf $p |- sqr : CC --> CC $= ... $.
41164 sqrth $p |- ( A e. CC -> ( ( sqr ` A ) ^ 2 ) = A ) $= ... $.
41165 sqrrege0 $p |- ( A e. CC -> 0 <_ ( Re ` ( sqr ` A ) ) ) $= ... $.
41166 eqsqror $p |- ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) = B <-> ( A = ( sqr ` B ) \/ A = -u ( sqr ` B ) ) ) ) $= ... $.
41176 eqsqrd $p |- ( ph -> A = ( sqr ` B ) ) $= ... $.
41179 eqsqr2d $p |- ( ph -> A = ( sqr ` B ) ) $= ... $.
41184 sqrthi $p |- ( 0 <_ A -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A ) $= ... $.
41185 sqrcli $p |- ( 0 <_ A -> ( sqr ` A ) e. RR ) $= ... $.
41186 sqrgt0i $p |- ( 0 < A -> 0 < ( sqr ` A ) ) $= ... $.
41187 sqrmsqi $p |- ( 0 <_ A -> ( sqr ` ( A x. A ) ) = A ) $= ... $.
41188 sqrsqi $p |- ( 0 <_ A -> ( sqr ` ( A ^ 2 ) ) = A ) $= ... $.
41189 sqsqri $p |- ( 0 <_ A -> ( ( sqr ` A ) ^ 2 ) = A ) $= ... $.
41190 sqrge0i $p |- ( 0 <_ A -> 0 <_ ( sqr ` A ) ) $= ... $.
41198 sqrpclii $p |- ( sqr ` A ) e. RR $= ... $.
41199 sqrgt0ii $p |- 0 < ( sqr ` A ) $= ... $.
41202 sqr11i $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqr ` A ) = ( sqr ` B ) <-> A = B ) ) $= ... $.
41203 sqrmuli $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) ) $= ... $.
41207 sqrmulii $p |- ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) $= ... $.
41209 sqrmsq2i $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( sqr ` A ) = B <-> A = ( B x. B ) ) ) $= ... $.
41210 sqrlei $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) ) $= ... $.
41211 sqrlti $p |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) ) $= ... $.
41241 rpsqrcld $p |- ( ph -> ( sqr ` A ) e. RR+ ) $= ... $.
41242 sqrgt0d $p |- ( ph -> 0 < ( sqr ` A ) ) $= ... $.
41254 resqrcld $p |- ( ph -> ( sqr ` A ) e. RR ) $= ... $.
41255 sqrmsqd $p |- ( ph -> ( sqr ` ( A x. A ) ) = A ) $= ... $.
41256 sqrsqd $p |- ( ph -> ( sqr ` ( A ^ 2 ) ) = A ) $= ... $.
41257 sqrge0d $p |- ( ph -> 0 <_ ( sqr ` A ) ) $= ... $.
41258 sqrnegd $p |- ( ph -> ( sqr ` -u A ) = ( _i x. ( sqr ` A ) ) ) $= ... $.
41262 sqrdivd $p |- ( ph -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) ) $= ... $.
41266 sqrmuld $p |- ( ph -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) ) $= ... $.
41267 sqrsq2d $p |- ( ph -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) ) $= ... $.
41268 sqrled $p |- ( ph -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) ) $= ... $.
41269 sqrltd $p |- ( ph -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) ) $= ... $.
41270 sqr11d.5 $e |- ( ph -> ( sqr ` A ) = ( sqr ` B ) ) $.
41290 sqrcld $p |- ( ph -> ( sqr ` A ) e. CC ) $= ... $.
41291 sqrrege0d $p |- ( ph -> 0 <_ ( Re ` ( sqr ` A ) ) ) $= ... $.
41292 sqsqrd $p |- ( ph -> ( ( sqr ` A ) ^ 2 ) = A ) $= ... $.
41293 msqsqrd $p |- ( ph -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A ) $= ... $.
41295 sqr00d.2 $e |- ( ph -> ( sqr ` A ) = 0 ) $.
44497 sqr2irrlem.3 $e |- ( ph -> ( sqr ` 2 ) = ( A / B ) ) $.
44502 sqr2irr $p |- ( sqr ` 2 ) e/ QQ $= ... $.
44504 sqr2re $p |- ( sqr ` 2 ) e. RR $= ... $.
45491 zsqrelqelz $p |- ( ( A e. ZZ /\ ( sqr ` A ) e. QQ ) -> ( sqr ` A ) e. ZZ ) $= ... $.
84684 cphsqrcl $p |- ( ( W e. CPreHil /\ ( A e. K /\ A e. RR /\ 0 <_ A ) ) -> ( sqr ` A ) e. K ) $= ... $.
84686 cphsqrcl2 $p |- ( ( W e. CPreHil /\ A e. K /\ -. -u A e. RR+ ) -> ( sqr ` A ) e. K ) $= ... $.
84687 cphsqrcl3 $p |- ( ( W e. CPreHil /\ _i e. K /\ A e. K ) -> ( sqr ` A ) e. K ) $= ... $.
91919 cxpsqrlem $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqr ` A ) ) -> ( _i x. ( sqr ` A ) ) e. RR ) $= ... $.
91920 cxpsqr $p |- ( A e. CC -> ( A ^c ( 1 / 2 ) ) = ( sqr ` A ) ) $= ... $.
91921 logsqr $p |- ( A e. RR+ -> ( log ` ( sqr ` A ) ) = ( ( log ` A ) / 2 ) ) $= ... $.
92016 dvsqr $p |- ( RR _D ( x e. RR+ |-> ( sqr ` x ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqr ` x ) ) ) ) $= ... $.
92054 resqrcn $p |- ( sqr |` ( 0 [,) +oo ) ) e. ( ( 0 [,) +oo ) -cn-> RR ) $= ... $.
92056 sqrcn $p |- ( sqr |` D ) e. ( D -cn-> CC ) $= ... $.
92100 loglesqr $p |- ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( A + 1 ) ) <_ ( sqr ` A ) ) $= ... $.
92831 sqrlim $p |- ( n e. RR+ |-> ( 1 / ( sqr ` n ) ) ) ~~>r 0 $= ... $.
92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $.
92870 divsqrsumlem $p |- ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqr ` A ) ) ) ) $= ... $.
92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $.
92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $.
92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $.
92874 divsqrsum2 $p |- ( ( ph /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqr ` A ) ) ) $= ... $.
92869 divsqrsum.2 $e |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) ) $.
92875 divsqrsumo1 $p |- ( ph -> ( y e. RR+ |-> ( ( ( F ` y ) - L ) x. ( sqr ` y ) ) ) e. O(1) ) $= ... $.
120881 dvcnsqr $p |- ( CC _D ( x e. D |-> ( sqr ` x ) ) ) = ( x e. D |-> ( 1 / ( 2 x. ( sqr ` x ) ) ) ) $= ... $.
124714 rmspecsqrnq $p |- ( A e. ( ZZ>= ` 2 ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) ) $= ... $.

[Alexander van der Vekens]

The special subtopic about "ring vs. rng" is tracked by GitHub issue #1389 now...

Alexander