Skip to content
Post PR summary comment

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

Sign in to view logs

[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 #6011

This job succeeded