search

math-comp / real-closed

Theorems for Real Closed Fields
13 stars 11 forks source link

modulus of the inverse, easy consequence of normcM #35

Closed ybertot closed 2 years ago

ybertot commented 3 years ago 
modified:   theories/complex.v
CohenCyril commented 3 years ago

These are supposed to be internal lemmas, to instanciate normedZmodType structures. Why can't you use the ones from the theory: normfV?

ybertot commented 3 years ago

(fun (x : complex R) => `|x|) has type R[i] -> R[i] (modulo conversion), but I am interested in the function of type complex R -> R, and I need the inversion property for this function. Does it make sense?

ybertot commented 3 years ago

So, normcV is the theorem that is really important to me, I don't really care about normCV, and only the latter is provided by normfV.

affeldt-aist commented 2 years ago

Should we postpone this PR to the next release (1.1.4)?

ybertot commented 2 years ago

A use case for this lemma is visible in Mohit Tekriwal's development. This is apparently used to ease the intermixing of developments relying on Coquelicot.

affeldt-aist commented 2 years ago

A use case for this lemma is visible in Mohit Tekriwal's development. This is apparently used to ease the intermixing of developments relying on Coquelicot.

Maybe you mean this link https://github.com/mohittkr/iterative_convergence.

ybertot commented 2 years ago

Yes you are right.

affeldt-aist commented 2 years ago

Should we provide a section before Section ComplexField with the theory of normc and keep only the normC theory inside the Section ComplexField?

affeldt-aist commented 2 years ago

Should we provide a section before Section ComplexField with the theory of normc and keep only the normC theory inside the Section ComplexField?

Something like https://github.com/math-comp/real-closed/pull/35/commits/4e9346fbf59fb9e1fce294472458f90fa05b516e ?

affeldt-aist commented 2 years ago

No opinion on this one? Should we postpone to the next release?