Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.inv_pos_of_nat

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.inv_pos_of_natView on Github →
2020-05-18 13:38
src/algebra/ordered_field.lean
refactor(algebra): merge init_.algebra into algebra (#2707) …
Modified nat.inv_pos_of_natView on Github →
2019-07-31 16:48
src/algebra/ordered_field.lean
doc(data/padics, data/real/cau_seq, algebra): add doc strings, remove unnecessary assumptions (#1283) …
Modified nat.inv_pos_of_natView on Github →
2019-07-03 00:58
src/algebra/ordered_field.lean
feat(measure_theory): Define Bochner integration (#1149) …
Added nat.inv_pos_of_natView on Github →