Commit 2025-04-24 17:05 e8eb83f3

View on Github →

chore: generalise results about x ^ n = ⊤ to WithTop (#24339) And mark them simp

Estimated changes

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

added theorem WithTop.eq_top_of_pow

added theorem WithTop.pow_eq_top_iff

added theorem WithTop.pow_lt_top

added theorem WithTop.pow_lt_top_iff

added theorem WithTop.pow_ne_top

added theorem WithTop.pow_ne_top_iff

modified theorem WithTop.top_pow

Modified Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/ENNReal/Operations.lean

added theorem ENNReal.eq_top_of_pow

deleted theorem ENNReal.pow_eq_top

modified theorem ENNReal.pow_eq_top_iff

modified theorem ENNReal.pow_lt_top

added theorem ENNReal.pow_lt_top_iff

modified theorem ENNReal.pow_ne_top

added theorem ENNReal.pow_ne_top_iff

modified theorem ENNReal.top_pow

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.eq_top_of_pow

added theorem ENat.pow_eq_top_iff

added theorem ENat.pow_lt_top_iff

added theorem ENat.pow_ne_top_iff

modified theorem ENat.top_pow

Modified Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/Probability/Variance.lean