Commit 2024-11-15 06:41 0ece1d71

feat: define IsLittleOTVS (#9675) The key theorem here is isLittleOTVS_iff_isLittleO, which enables us in a future PR to redefine HasFDerivAtFilter to not be dependent on a choice of norm, making it possible to state results about derivatives of types with no canonical norm. This gives us a middle ground of being able to state Matrix.hasDerivAt_add, which is better than not being able to state it, but not as good as being able to reuse the global hasDerivAt_add. Later on, we can try to generalize results like IsLittleO.add to IsLittleOTVS, which would help with this reuse. Zulip thread