Theorem WithZero.ofAdd_neg_one_pow_comm

Modification history

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_comm View on Github →