Theorem Real.sign_zero

Modification history

2026-08-11 00:21

Mathlib/Data/Real/Sign.lean

chore: bump toolchain to v4.34.0-rc1 (#42619)

Modified Real.sign_zero View on Github →

2023-01-17 10:40

Mathlib/Data/Real/Sign.lean

feat: port Data.Real.Sign (#1618)

Added Real.sign_zero View on Github →