Documentation
Batteries
.
Data
.
Int
.
Order
Search
Google site search
return to top
source
Imports
Init
Batteries.Tactic.Alias
Imported by
Int
.
ofNat_natAbs_eq_of_nonneg
source
@[deprecated Int.natAbs_of_nonneg]
theorem
Int
.
ofNat_natAbs_eq_of_nonneg
{a :
Int
}
(H :
0
≤
a
)
:
↑
a
.natAbs
=
a
Alias
of
Int.natAbs_of_nonneg
.