Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sub_half

Modification history

2020-10-08 10:23

src/algebra/char_zero.lean

chore(algebra/char_zero): rename vars, add `with_top` instance (#4523) …

Modified sub_half View on Github →

2018-01-21 23:57

algebra/char_zero.lean

feat(data/real): real square root function, sqrt 2 is irrational

Added sub_half View on Github →