Commit 2024-07-20 19:55 1141ca2b

View on Github →

chore(GroupTheory/OrderOfElement): remove ' from pow_ne_one_of_lt_orderOf' (#14955) We change the name of pow_ne_one_of_lt_orderOf' to pow_ne_one_of_lt_orderOf. See here on Zulip.

Estimated changes

Modified Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

Modified Mathlib/GroupTheory/Exponent.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

deleted theorem pow_ne_one_of_lt_orderOf'

added theorem pow_ne_one_of_lt_orderOf

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean