Commit 2024-09-20 18:56 f8da9a58

View on Github →

feat(Order/Group): add zpow_right_strictAnti (#16937) Also use it to golf Subgroup.mem_closure_singleton_iff_existsUnique_zpow.

Estimated changes

Modified Mathlib/Algebra/Order/Group/Basic.lean

added theorem zpow_right_strictAnti

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

Modified Mathlib/MeasureTheory/Integral/Periodic.lean

Modified Mathlib/Topology/Instances/AddCircle.lean