Documentation

Std.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 Std/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
    @[simp]
    theorem List.nonzeroMinimum_eq_zero_iff {xs : List Nat} :
    List.nonzeroMinimum xs = 0 ∀ (x : Nat), x xsx = 0
    theorem List.nonzeroMinimum_pos {a : Nat} {xs : List Nat} (m : a xs) (h : a 0) :
    theorem List.nonzeroMinimum_le {a : Nat} {xs : List Nat} (m : a xs) (h : a 0) :
    theorem List.nonzeroMinimum_eq_nonzero_iff {xs : List Nat} {y : Nat} (h : y 0) :
    List.nonzeroMinimum xs = y y xs ∀ (x : Nat), x xsy x x = 0
    theorem List.nonzeroMininum_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 List.minNatAbs_eq_zero_iff {xs : List Int} :
      List.minNatAbs xs = 0 ∀ (y : Int), y xsy = 0
      theorem List.minNatAbs_eq_nonzero_iff {z : Nat} (xs : List Int) (w : z 0) :
      List.minNatAbs xs = z (∃ (y : Int), y xs Int.natAbs y = z) ∀ (y : Int), y xsz Int.natAbs y y = 0

      The maximum absolute value in a list of integers.

      Equations
      Instances For