Documentation

Mathlib.Tactic.LinearCombination.Lemmas

Lemmas for the linear_combination tactic #

These should not be used directly in user code.

Addition #

source
theorem Mathlib.Tactic.LinearCombination.add_eq_eq {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [Add α] (p₁ : a₁ = b₁) (p₂ : a₂ = b₂) :
a₁ + a₂ = b₁ + b₂
source
theorem Mathlib.Tactic.LinearCombination.add_le_eq {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (p₁ : a₁ ≤ b₁) (p₂ : a₂ = b₂) :
a₁ + a₂ ≤ b₁ + b₂
source
theorem Mathlib.Tactic.LinearCombination.add_eq_le {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] (p₁ : a₁ = b₁) (p₂ : a₂ ≤ b₂) :
a₁ + a₂ ≤ b₁ + b₂
source
theorem Mathlib.Tactic.LinearCombination.add_lt_eq {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p₁ : a₁ < b₁) (p₂ : a₂ = b₂) :
a₁ + a₂ < b₁ + b₂
source
theorem Mathlib.Tactic.LinearCombination.add_eq_lt {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {a₁ b₁ a₂ b₂ : α} (p₁ : a₁ = b₁) (p₂ : a₂ < b₂) :
a₁ + a₂ < b₁ + b₂

Multiplication #

source
theorem Mathlib.Tactic.LinearCombination.mul_eq_const {α : Type u_1} {a b : α} [Mul α] (p : a = b) (c : α) :
a * c = b * c
source
theorem Mathlib.Tactic.LinearCombination.mul_le_const {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) :
b * a ≤ c * a
source
theorem Mathlib.Tactic.LinearCombination.mul_lt_const {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] (p : b < c) {a : α} (ha : 0 < a) :
b * a < c * a
source
theorem Mathlib.Tactic.LinearCombination.mul_lt_const_weak {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (p : b < c) {a : α} (ha : 0 ≤ a) :
b * a ≤ c * a
source
theorem Mathlib.Tactic.LinearCombination.mul_const_eq {α : Type u_1} {b c : α} [Mul α] (p : b = c) (a : α) :
a * b = a * c
source
theorem Mathlib.Tactic.LinearCombination.mul_const_le {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) :
a * b ≤ a * c
source
theorem Mathlib.Tactic.LinearCombination.mul_const_lt {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] (p : b < c) {a : α} (ha : 0 < a) :
a * b < a * c
source
theorem Mathlib.Tactic.LinearCombination.mul_const_lt_weak {α : Type u_1} {b c : α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (p : b < c) {a : α} (ha : 0 ≤ a) :
a * b ≤ a * c

Scalar multiplication #

source
theorem Mathlib.Tactic.LinearCombination.smul_eq_const {α : Type u_1} {K : Type u_2} {t s : K} [SMul K α] (p : t = s) (c : α) :
t • c = s • c
source
theorem Mathlib.Tactic.LinearCombination.smul_le_const {α : Type u_1} {K : Type u_2} {t s : K} [Ring K] [PartialOrder K] [IsOrderedRing K] [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [Module K α] [OrderedSMul K α] (p : t ≤ s) {a : α} (ha : 0 ≤ a) :
t • a ≤ s • a
source
theorem Mathlib.Tactic.LinearCombination.smul_lt_const {α : Type u_1} {K : Type u_2} {t s : K} [Ring K] [PartialOrder K] [IsOrderedRing K] [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [Module K α] [OrderedSMul K α] (p : t < s) {a : α} (ha : 0 < a) :
t • a < s • a
source
theorem Mathlib.Tactic.LinearCombination.smul_lt_const_weak {α : Type u_1} {K : Type u_2} {t s : K} [Ring K] [PartialOrder K] [IsOrderedRing K] [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [Module K α] [OrderedSMul K α] (p : t < s) {a : α} (ha : 0 ≤ a) :
t • a ≤ s • a
source
theorem Mathlib.Tactic.LinearCombination.smul_const_eq {α : Type u_1} {b c : α} {K : Type u_2} [SMul K α] (p : b = c) (s : K) :
s • b = s • c
source
theorem Mathlib.Tactic.LinearCombination.smul_const_le {α : Type u_1} {b c : α} {K : Type u_2} [Semiring K] [PartialOrder K] [AddCommMonoid α] [PartialOrder α] [Module K α] [OrderedSMul K α] (p : b ≤ c) {s : K} (hs : 0 ≤ s) :
s • b ≤ s • c
source
theorem Mathlib.Tactic.LinearCombination.smul_const_lt {α : Type u_1} {b c : α} {K : Type u_2} [Semiring K] [PartialOrder K] [AddCommMonoid α] [PartialOrder α] [Module K α] [OrderedSMul K α] (p : b < c) {s : K} (hs : 0 < s) :
s • b < s • c
source
theorem Mathlib.Tactic.LinearCombination.smul_const_lt_weak {α : Type u_1} {b c : α} {K : Type u_2} [Semiring K] [PartialOrder K] [AddCommMonoid α] [PartialOrder α] [Module K α] [OrderedSMul K α] (p : b < c) {s : K} (hs : 0 ≤ s) :
s • b ≤ s • c

Division #

source
theorem Mathlib.Tactic.LinearCombination.div_eq_const {α : Type u_1} {a b : α} [Div α] (p : a = b) (c : α) :
a / c = b / c
source
theorem Mathlib.Tactic.LinearCombination.div_le_const {α : Type u_1} {b c : α} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) :
b / a ≤ c / a
source
theorem Mathlib.Tactic.LinearCombination.div_lt_const {α : Type u_1} {b c : α} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (p : b < c) {a : α} (ha : 0 < a) :
b / a < c / a
source
theorem Mathlib.Tactic.LinearCombination.div_lt_const_weak {α : Type u_1} {b c : α} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] (p : b < c) {a : α} (ha : 0 ≤ a) :
b / a ≤ c / a

Lemmas constructing the reduction of a goal to a specified built-up hypothesis #

source
theorem Mathlib.Tactic.LinearCombination.eq_of_eq {α : Type u_1} {a a' b b' : α} [Add α] [IsRightCancelAdd α] (p : a = b) (H : a' + b = b' + a) :
a' = b'
source
theorem Mathlib.Tactic.LinearCombination.le_of_le {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a ≤ b) (H : a' + b ≤ b' + a) :
a' ≤ b'
source
theorem Mathlib.Tactic.LinearCombination.le_of_eq {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a = b) (H : a' + b ≤ b' + a) :
a' ≤ b'
source
theorem Mathlib.Tactic.LinearCombination.le_of_lt {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a < b) (H : a' + b ≤ b' + a) :
a' ≤ b'
source
theorem Mathlib.Tactic.LinearCombination.lt_of_le {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a ≤ b) (H : a' + b < b' + a) :
a' < b'
source
theorem Mathlib.Tactic.LinearCombination.lt_of_eq {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a = b) (H : a' + b < b' + a) :
a' < b'
source
theorem Mathlib.Tactic.LinearCombination.lt_of_lt {α : Type u_1} {a a' b b' : α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] (p : a < b) (H : a' + b ≤ b' + a) :
a' < b'
source
theorem Mathlib.Tactic.LinearCombination.eq_rearrange {G : Type u_3} [AddGroup G] {a b : G} :
a - b = 0 → a = b

Alias of the forward direction of sub_eq_zero.

source
theorem Mathlib.Tactic.LinearCombination.le_rearrange {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a - b ≤ 0) :
a ≤ b
source
theorem Mathlib.Tactic.LinearCombination.lt_rearrange {α : Type u_3} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a - b < 0) :
a < b
source
theorem Mathlib.Tactic.LinearCombination.eq_of_add_pow {α : Type u_1} {a a' b b' : α} [Ring α] [NoZeroDivisors α] (n : ℕ) (p : a = b) (H : (a' - b') ^ n - (a - b) = 0) :
a' = b'

Lookup functions for lemmas by operation and relation(s) #

source
def Mathlib.Ineq.addRelRelData :
Ineq → Ineq → Lean.Name

Given two (in)equalities, look up the lemma to add them.

Equations
Instances For
    source
    inductive Mathlib.Ineq.WithStrictness :
    Type

    Finite inductive type extending Mathlib.Ineq: a type of inequality (eq, le or lt), together with, in the case of lt, a boolean, typically representing the strictness (< or ≤) of some other inequality.

    Instances For
      source
      def Mathlib.Ineq.mulRelConstData :
      Ineq.WithStrictness → Lean.Name

      Given an (in)equality, look up the lemma to left-multiply it by a constant. If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

      Equations
      Instances For
        source
        def Mathlib.Ineq.mulConstRelData :
        Ineq.WithStrictness → Lean.Name

        Given an (in)equality, look up the lemma to right-multiply it by a constant. If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

        Equations
        Instances For
          source
          def Mathlib.Ineq.smulRelConstData :
          Ineq.WithStrictness → Lean.Name

          Given an (in)equality, look up the lemma to left-scalar-multiply it by a constant (scalar). If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

          Equations
          Instances For
            source
            def Mathlib.Ineq.smulConstRelData :
            Ineq.WithStrictness → Lean.Name

            Given an (in)equality, look up the lemma to right-scalar-multiply it by a constant (vector). If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

            Equations
            Instances For
              source
              def Mathlib.Ineq.divRelConstData :
              Ineq.WithStrictness → Lean.Name

              Given an (in)equality, look up the lemma to divide it by a constant. If relevant, also take into account the degree of positivity which can be proved of the constant: strict or non-strict.

              Equations
              Instances For
                source
                def Mathlib.Ineq.relImpRelData :
                Ineq → Ineq → Option (Lean.Name × Ineq)

                Given two (in)equalities P and Q, look up the lemma to deduce Q from P, and the relation appearing in the side condition produced by this lemma.

                Equations
                Instances For
                  source
                  def Mathlib.Ineq.rearrangeData :
                  Ineq → Lean.Name

                  Given an (in)equality, look up the lemma to move everything to the LHS.

                  Equations
                  Instances For