Commit 2026-04-17 16:37 0cafeeef

View on Github →

chore: remove some backward.proofsInPublic (#38156)

Estimated changes

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem IsMulTorsionFree.orderOf_le_one

added theorem isOfFinOrder_iff_eq_one

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

modified def mulEquivOfOrderOfEq

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