Commit 2024-10-22 15:31 520965a9

View on Github →

chore: deprecate WithTop.zero_lt_{coe,top} for WithTop.{coe,top}_pos (#18048) The two are almost identical, except zero_lt_coe has an explicit argument where coe_pos has it implicit. Both the name and implicitness of coe_pos fit our style better. Also zero_lt_coe seems to be used only once in Mathlib. Found when cleaning up simp porting notes.

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

added theorem WithTop.one_lt_top

deleted theorem WithTop.zero_lt_top

Modified Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Normed/Algebra/Exponential.lean

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.top_pos

deleted theorem ENat.zero_lt_top

Modified Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Measure/Count.lean

Modified Mathlib/Topology/MetricSpace/Infsep.lean