Theorem NNReal.zpow_pos

Modification history

2024-10-11 15:01

Mathlib/Data/NNReal/Basic.lean

chore: generalise `zpow` lemmas from `LinearOrderedSemifield` to `GroupWithZero` (#17539)

Deleted NNReal.zpow_pos View on Github →

2023-02-20 08:04

Mathlib/Data/Real/NNReal.lean

feat: port Data.Real.NNReal (#2234)

Added NNReal.zpow_pos View on Github →