Theorem Nat.clog_pos

Modification history

2025-11-24 15:41

Mathlib/Data/Nat/Log.lean

refactor(Nat/Log): redefine `Nat.log` and `Nat.clog` (#31990) …

Modified Nat.clog_pos View on Github →

2022-12-19 15:36

Mathlib/Data/Nat/Log.lean

feat: port Data.Nat.Log (#1089) …

Added Nat.clog_pos View on Github →