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₂ : α} [OrderedAddCommMonoid α] (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₂ : α} [OrderedAddCommMonoid α] (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₂ : α} [OrderedCancelAddCommMonoid α] (p₁ : a₁ < b₁) (p₂ : a₂ = b₂) :
a₁ + a₂ < b₁ + b₂
source
theorem Mathlib.Tactic.LinearCombination.add_eq_lt {α : Type u_1} [OrderedCancelAddCommMonoid α] {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 : α} [OrderedSemiring α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) :
b * a ≤ c * a
source
theorem Mathlib.Tactic.LinearCombination.mul_lt_const {α : Type u_1} {b c : α} [StrictOrderedSemiring α] (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 : α} [OrderedSemiring α] (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 : α} [OrderedSemiring α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) :
a * b ≤ a * c
source
theorem Mathlib.Tactic.LinearCombination.mul_const_lt {α : Type u_1} {b c : α} [StrictOrderedSemiring α] (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 : α} [OrderedSemiring α] (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} [OrderedRing K] [OrderedAddCommGroup α] [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} [OrderedRing K] [OrderedAddCommGroup α] [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} [OrderedRing K] [OrderedAddCommGroup α] [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} [OrderedSemiring K] [OrderedAddCommMonoid α] [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} [OrderedSemiring K] [OrderedAddCommMonoid α] [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} [OrderedSemiring K] [OrderedAddCommMonoid α] [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 : α} [LinearOrderedSemifield α] (p : b ≤ c) {a : α} (ha : 0 ≤ a) :
b / a ≤ c / a
source
theorem Mathlib.Tactic.LinearCombination.div_lt_const {α : Type u_1} {b c : α} [LinearOrderedSemifield α] (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 : α} [LinearOrderedSemifield α] (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' : α} [OrderedCancelAddCommMonoid α] (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' : α} [OrderedCancelAddCommMonoid α] (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' : α} [OrderedCancelAddCommMonoid α] (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' : α} [OrderedCancelAddCommMonoid α] (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' : α} [OrderedCancelAddCommMonoid α] (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' : α} [OrderedCancelAddCommMonoid α] (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} [OrderedAddCommGroup α] {a b : α} (h : a - b ≤ 0) :
a ≤ b
source
theorem Mathlib.Tactic.LinearCombination.lt_rearrange {α : Type u_3} [OrderedAddCommGroup α] {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
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.

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
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
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
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
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
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
source
def Mathlib.Ineq.rearrangeData :
Ineq → Lean.Name

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

Equations