Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-31 09:47 1b49d480

View on Github →

refactor(group_theory/order_of_element): Remove coercion in order_eq_card_zpowers (#14364) This PR removes a coercion in order_eq_card_zpowers.

Estimated changes

modified theorem order_eq_card_zpowers