Theorem pow_succ''

Modification history

2023-09-06 04:50

Mathlib/Algebra/GroupWithZero/Defs.lean

chore: ensure Ring/Defs doesn't depend on Group/Basic (#6956) …

Deleted pow_succ''View on Github →

2022-10-14 00:13

Mathlib/Algebra/GroupWithZero/Defs.lean

feat: replace Algebra/Group/{Defs,Basic} with direct ports from mathlib3 (#457) …

Added pow_succ''View on Github →