analysis

analysis copied to clipboard

realType structure over fourcolor's reals

1

During an internship with @CohenCyril, I worked on proving the equivalence between math-comp's realType and fourcolor's Real.model. The original idea was to transfer [Fourcolor](https://github.com/rocq-community/fourcolor)'s proof of categoricity for their reals...

lweqx

- Definition of the sequence of prime numbers, ``prime_seq`` - Proof of its growth and correctness - Proof of the divergence of the sum of the reciprocals of prime numbers...

LucasMalaizier

https://github.com/math-comp/analysis/blob/7528cc1f76fb9f2edeb47e1fca81907ac5b8a81e/theories/derive.v#L1406 https://github.com/math-comp/analysis/blob/7528cc1f76fb9f2edeb47e1fca81907ac5b8a81e/theories/derive.v#L1415 https://github.com/math-comp/analysis/blob/7528cc1f76fb9f2edeb47e1fca81907ac5b8a81e/theories/derive.v#L1422 These three lines refer to derivation using GRing.exp but naming is inconsistent between them.

yosakaon