Mathlib v3 is deprecated. Go to Mathlib v4

Def int.sqrt

Modification history

2021-06-17 17:10

src/data/int/sqrt.lean

docs(data/*/sqrt): add one module docstring and expand the other (#7973)

Modified int.sqrt View on Github →

2020-07-09 13:55

src/data/int/sqrt.lean

feat(data): Mark all `sqrt`s as `@[pp_nodot]` (#3337)

Modified int.sqrt View on Github →

2018-11-05 08:59

data/int/sqrt.lean

feat(data/real/irrational): add basic irrational facts (#453) …

Added int.sqrt View on Github →