Theorem WithZero.ofAdd_neg_one_pow_comm

Modification history

2025-12-29 03:44
Mathlib/Algebra/GroupWithZero/Int.lean
chore: remove May 2025 deprecated declarations (#33014) …
Deleted WithZero.ofAdd_neg_one_pow_commView on Github →
2025-02-04 18:27
Mathlib/Algebra/GroupWithZero/Int.lean
feat(Algebra/GroupWithZero/Int): add lemmas about Zm0 (#21370)
Added WithZero.ofAdd_neg_one_pow_commView on Github →