Commit 2025-11-07 15:55 66464acf

View on Github →

chore(Data): deprecate toReal_eq_toReal, count_eq_of_nodup and smul_mat_cons (#28484)

Estimated changes

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Mathlib/Data/ENNReal/Real.lean

deleted theorem ENNReal.toReal_eq_toReal

Modified Mathlib/Data/List/Dedup.lean

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/List/Nodup.lean

deleted theorem List.count_eq_of_nodup

Modified Mathlib/LinearAlgebra/Matrix/Notation.lean

deleted theorem Matrix.smul_mat_cons

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

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/Probability/Distributions/Exponential.lean

Modified Mathlib/Probability/Independence/Integration.lean

Modified Mathlib/Probability/Kernel/Condexp.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean