Skip to content

[Merged by Bors] - chore(Analysis/Calculus/FDeriv/Extend): use Lean 4 naming scheme #42397

[Merged by Bors] - chore(Analysis/Calculus/FDeriv/Extend): use Lean 4 naming scheme

[Merged by Bors] - chore(Analysis/Calculus/FDeriv/Extend): use Lean 4 naming scheme #42397

Annotations

1 error and 1 warning

This job succeeded