Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.one_div_lt_one_div

Modification history

2022-06-23 16:23
src/data/nat/cast.lean
chore(data/nat,int): move field-specific lemmas about cast (#14890) …
Modified nat.one_div_lt_one_divView on Github →
2020-05-18 13:38
src/algebra/ordered_field.lean
refactor(algebra): merge init_.algebra into algebra (#2707) …
Modified nat.one_div_lt_one_divView on Github →
2019-08-08 02:35
src/algebra/ordered_field.lean
feat (analysis/normed_space): Define real inner product space (#1248) …
Added nat.one_div_lt_one_divView on Github →