Skip to content

'derivemxE' new name proposal #1647

@yosakaon

Description

@yosakaon

What about renaming derivemxE to deriveEjacobian ?

analysis/theories/derive.v

Lines 356 to 357 in 14c5bf8

Lemma derivemxE m n (f : 'rV[R]_m.+1 -> 'rV[R]_n.+1) (a v : 'rV[R]_m.+1) :
differentiable f a -> 'D_ v f a = v *m jacobian f a.

In my opinion, it is more appropriate because we can see by the name which alternative definition of directional derivative we're about to use (by the way, deriveE could maybe become deriveEdiff. to me both are equally valid alternative definitions of directional derivatives).

Metadata

Metadata

Assignees

No one assigned

    Labels

    renaming/refactoring 🔧This is about a renaming or refactoring in the library

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions