Commit 2025-06-18 09:36 bb38781a
View on Github →chore: add fun_
variants for Fréchet derivative of addition and like (#25865)
This follows the new convention explained at https://leanprover-community.github.io/contribute/naming.html#unexpanded-and-expanded-forms-of-functions