Commit 2026-09-09 09:50 10a27d43
View on Github →chore(Analysis/Calculus/FDeriv/Prod): deprecate differentiable*_finCons' as duplicates (#42583)
The four primed differentiable*_finCons' lemmas are exact copies of the unprimed ones (@…' = @… := by with_reducible rfl). Replaced by deprecated aliases, and repointed four in-file uses.
Aristotle found this duplication.