Theorem Nat.pow_succ'

Modification history

2022-09-04 16:26

Mathlib/Init/Data/Nat/Lemmas.lean

feat: depend on std4 (#397)

Deleted Nat.pow_succ'View on Github →

2022-06-13 19:31

Mathlib/Init/Data/Nat/Lemmas.lean

feat: port misc linters (#276)

Added Nat.pow_succ'View on Github →

2022-02-23 09:06

Mathlib/Algebra/Ring/Basic.lean

feat: `AddMonoidWithOne`, `AddGroupWithOne` (#206) …

Deleted Nat.pow_succ'View on Github →

2022-02-01 18:42

Mathlib/Algebra/Ring/Basic.lean

refactor: remove numeric (#177) …

Added Nat.pow_succ'View on Github →