Commit 2026-02-11 13:28 4071ce74

View on Github →

chore: deprecate duplicated lemma (#35126)

Estimated changes

Modified Mathlib/Analysis/Analytic/CPolynomialDef.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Analytic/Inverse.lean

Modified Mathlib/Analysis/Analytic/Within.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

deleted theorem edist_one_eq_enorm

Modified Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Normed.lean

Modified scripts/nolints_prime_decls.txt