Documentation

Lean.Elab.Tactic.Omega.MinNatAbs

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
Instances For
    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 xsy x x = 0
    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 xsp a 0q (f a) p a) :

    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
      @[simp]
      theorem Lean.Elab.Tactic.Omega.List.minNatAbs_eq_zero_iff {xs : List Int} :
      minNatAbs xs = 0 ∀ (y : Int), y xsy = 0
      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 xsz y.natAbs y = 0

      The maximum absolute value in a list of integers.

      Equations
      Instances For