Commit 2026-05-26 08:09 2df375a5

View on Github →

chore(Analysis/Normed/Group): deprecate duplicate ofReal_norm_eq_enorm (#39838) ofReal_norm was kept for symmetry with toReal_enorm, but was given a direct proof.

Estimated changes

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

modified theorem ofReal_norm'

deleted theorem ofReal_norm_eq_enorm'

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

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

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

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Indicator.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/Complete.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/SumMeasure.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Norm.lean

Modified Mathlib/MeasureTheory/Integral/Prod.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

Modified Mathlib/Probability/Distributions/Fernique.lean

Modified Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean

Modified Mathlib/Probability/Kernel/Disintegration/CondCDF.lean

Modified Mathlib/Probability/Moments/Tilted.lean

Modified scripts/nolints_prime_decls.txt