Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-15 08:51 7559d1c8

View on Github →

lint(data/num/*): add docs and remove some [has_zero] requirements (#4604)

Estimated changes

Modified src/data/num/basic.lean

modified def cast_num

deleted def pos_num.sqrt_aux1

deleted def pos_num.sqrt_aux

Modified src/data/num/bitwise.lean

Modified src/data/num/lemmas.lean

modified theorem pos_num.cast_bit0

modified theorem pos_num.cast_bit1

modified theorem pos_num.cast_one'

modified theorem pos_num.cast_one