List.nonzeroMinimum
, List.minNatAbs
, List.maxNatAbs
#
List.minNatAbs
computes the minimum non-zero absolute value of a List Int
.
This is not generally useful outside of the implementation of the omega
tactic,
so we keep it in the Lean/Elab/Tactic/Omega
directory
(although the definitions are in the List
namespace).
The minimum non-zero entry in a list of natural numbers, or zero if all entries are zero.
We completely characterize the function via
nonzeroMinimum_eq_zero_iff
and nonzeroMinimum_eq_nonzero_iff
below.
Equations
- Lean.Elab.Tactic.Omega.List.nonzeroMinimum xs = (List.filter (fun (x : Nat) => decide (x ≠ 0)) xs).min?.getD 0
Instances For
@[simp]
theorem
Lean.Elab.Tactic.Omega.List.nonzeroMinimum_mem
{xs : List Nat}
(w : nonzeroMinimum xs ≠ 0)
:
The minimum absolute value of a nonzero entry, or zero if all entries are zero.
We completely characterize the function via
minNatAbs_eq_zero_iff
and minNatAbs_eq_nonzero_iff
below.
Equations
Instances For
The maximum absolute value in a list of integers.