Added differentiability of the max function#1819

Open

lstrsrmn wants to merge 13 commits intomath-comp:masterfrom

lstrsrmn:max_differentiable

Commits on Feb 27, 2026

Added differentiability of the max function

lstrsrmn
authored and
affeldt-aist
committed
linting
affeldt-aist
committed
Added min derivable, generalised derive lemmas that rely on v != 0

lstrsrmn
authored and
affeldt-aist
committed
Added lemma to swap mathcomp natural log with Rocqs natural log

lstrsrmn
authored and
affeldt-aist
committed
Revert "Merge branch 'ln_eq_Rln' into HEAD"

lstrsrmn
authored and
affeldt-aist
committed
Updated changelog

lstrsrmn
authored and
affeldt-aist
committed
Fixed erroneous paces

lstrsrmn
authored and
affeldt-aist
committed
Fixed issue finding lemma

lstrsrmn
authored and
affeldt-aist
committed
Fixed error

lstrsrmn
authored and
affeldt-aist
committed
Removed dependence on direction that's no longer needed

lstrsrmn
authored and
affeldt-aist
committed
linting
affeldt-aist
committed
fix changelog
affeldt-aist
committed
fix
affeldt-aist
committed