Lynda

icon indicating a website link yosakaon.github.io

icon company Université Paris Cité icon location Paris, France icon location LOGOS master student @ Paris 7 Currently interning @ AIST Tokyo

Results 3 issues of Lynda

'derivemxE' new name proposal

What about renaming `derivemxE` to `deriveEjacobian` ? https://github.com/math-comp/analysis/blob/14c5bf819bce88100955bc655f0307568e13391c/theories/derive.v#L356 In my opinion, it is more appropriate because we can see by the name which alternative definition of directional derivative we're about...

differentiable rsubmx/lsubmx lemmas + derive_sqrt

##### Motivation for this change When deriving differential equations using lsubmx/rsubmx, we need proofs of their differentiability. This PR also contains a lemma making use of the "is_derive1_sqrt" lemma to...

'exprn' and 'expr' naming inconsistency in derive.v

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.