# `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).

source
def Lean.Elab.Tactic.Omega.List.nonzeroMinimum (xs : List Nat) :
Nat

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

source
@[simp]
theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_zero_iff {xs : List Nat} :
nonzeroMinimum xs = 0 ↔ ∀ (x : Nat), x ∈ xs → x = 0
source
theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_mem {xs : List Nat} (w : nonzeroMinimum xs ≠ 0) :
nonzeroMinimum xs ∈ xs
source
theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_pos {a : Nat} {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) :
0 < nonzeroMinimum xs
source
theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_le {a : Nat} {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) :
nonzeroMinimum xs ≤ a
source
theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_nonzero_iff {xs : List Nat} {y : Nat} (h : y ≠ 0) :
nonzeroMinimum xs = y ↔ y ∈ xs ∧ ∀ (x : Nat), x ∈ xs → y ≤ x ∨ x = 0
source
theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_eq_of_nonzero {xs : List Nat} (h : nonzeroMinimum xs ≠ 0) :
∃ (x : Nat), x ∈ xs ∧ nonzeroMinimum xs = x
source
theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_le_iff {xs : List Nat} {y : Nat} :
nonzeroMinimum xs ≤ y ↔ nonzeroMinimum xs = 0 ∨ ∃ (x : Nat), x ∈ xs ∧ x ≤ y ∧ x ≠ 0
source
theorem Lean.Elab.Tactic.Omega.List.nonzeroMinimum_map_le_nonzeroMinimum {α : Type u_1} {β : Type u_2} (f : α → β) (p : α → Nat) (q : β → Nat) (xs : List α) (h : ∀ (a : α), a ∈ xs → (p a = 0 ↔ q (f a) = 0)) (w : ∀ (a : α), a ∈ xs → p a ≠ 0 → q (f a) ≤ p a) :
nonzeroMinimum (List.map q (List.map f xs)) ≤ nonzeroMinimum (List.map p xs)
source
def Lean.Elab.Tactic.Omega.List.minNatAbs (xs : List Int) :
Nat

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

- Lean.Elab.Tactic.Omega.List.minNatAbs xs = Lean.Elab.Tactic.Omega.List.nonzeroMinimum (List.map Int.natAbs xs)

Instances For

source
@[simp]
theorem Lean.Elab.Tactic.Omega.List.minNatAbs_eq_zero_iff {xs : List Int} :
minNatAbs xs = 0 ↔ ∀ (y : Int), y ∈ xs → y = 0
source
theorem Lean.Elab.Tactic.Omega.List.minNatAbs_eq_nonzero_iff {z : Nat} (xs : List Int) (w : z ≠ 0) :
minNatAbs xs = z ↔ (∃ (y : Int), y ∈ xs ∧ y.natAbs = z) ∧ ∀ (y : Int), y ∈ xs → z ≤ y.natAbs ∨ y = 0
source
@[simp]
theorem Lean.Elab.Tactic.Omega.List.minNatAbs_nil :
minNatAbs [] = 0
source
def Lean.Elab.Tactic.Omega.List.maxNatAbs (xs : List Int) :
Nat

The maximum absolute value in a list of integers.

Equations

- Lean.Elab.Tactic.Omega.List.maxNatAbs xs = (List.map Int.natAbs xs).max?.getD 0

Instances For