ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>AddGroup α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(OrderIso.addLeft a).symm = OrderIso.addLeft (-a)
<VAR>α : Type u<VAR>Group α<VAR>LE α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>(OrderIso.mulLeft a).symm = OrderIso.mulLeft a⁻¹
<VAR>α : Type u_1<VAR>One α<GOAL>OrderDual.toDual 1 = 1
<VAR>α : Type u_1<VAR>Zero α<GOAL>OrderDual.toDual 0 = 0
<VAR>α : Type u_1<VAR>Zero α<GOAL>OrderDual.ofDual 0 = 0
<VAR>α : Type u_1<VAR>One α<GOAL>OrderDual.ofDual 1 = 1
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : α<GOAL>OrderDual.toDual (a * b) = OrderDual.toDual a * OrderDual.toDual b
<VAR>α : Type u_1<VAR>Add α<VAR>a b : α<GOAL>OrderDual.toDual (a + b) = OrderDual.toDual a + OrderDual.toDual b
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a * b) = OrderDual.ofDual a * OrderDual.ofDual b
<VAR>α : Type u_1<VAR>Add α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a + b) = OrderDual.ofDual a + OrderDual.ofDual b
<VAR>α : Type u_1<VAR>Inv α<VAR>a : α<GOAL>OrderDual.toDual a⁻¹ = (OrderDual.toDual a)⁻¹
<VAR>α : Type u_1<VAR>Neg α<VAR>a : α<GOAL>OrderDual.toDual (-a) = -OrderDual.toDual a
<VAR>α : Type u_1<VAR>Neg α<VAR>a : αᵒᵈ<GOAL>OrderDual.ofDual (-a) = -OrderDual.ofDual a
<VAR>α : Type u_1<VAR>Inv α<VAR>a : αᵒᵈ<GOAL>OrderDual.ofDual a⁻¹ = (OrderDual.ofDual a)⁻¹
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : α<GOAL>OrderDual.toDual (a - b) = OrderDual.toDual a - OrderDual.toDual b
<VAR>α : Type u_1<VAR>Div α<VAR>a b : α<GOAL>OrderDual.toDual (a / b) = OrderDual.toDual a / OrderDual.toDual b
<VAR>α : Type u_1<VAR>Div α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a / b) = OrderDual.ofDual a / OrderDual.ofDual b
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a - b) = OrderDual.ofDual a - OrderDual.ofDual b
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : β<VAR>a : α<GOAL>OrderDual.toDual (b +ᵥ a) = b +ᵥ OrderDual.toDual a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : α<VAR>b : β<GOAL>OrderDual.toDual (a ^ b) = OrderDual.toDual a ^ b
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : β<VAR>a : α<GOAL>OrderDual.toDual (b • a) = b • OrderDual.toDual a
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : β<VAR>a : αᵒᵈ<GOAL>OrderDual.ofDual (b +ᵥ a) = b +ᵥ OrderDual.ofDual a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : αᵒᵈ<VAR>b : β<GOAL>OrderDual.ofDual (a ^ b) = OrderDual.ofDual a ^ b
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : β<VAR>a : αᵒᵈ<GOAL>OrderDual.ofDual (b • a) = b • OrderDual.ofDual a
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : β<VAR>a : α<GOAL>OrderDual.toDual b • a = b • a
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : β<VAR>a : α<GOAL>OrderDual.toDual b +ᵥ a = b +ᵥ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : α<VAR>b : β<GOAL>a ^ OrderDual.toDual b = a ^ b
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : βᵒᵈ<VAR>a : α<GOAL>OrderDual.ofDual b • a = b • a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : α<VAR>b : βᵒᵈ<GOAL>a ^ OrderDual.ofDual b = a ^ b
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : βᵒᵈ<VAR>a : α<GOAL>OrderDual.ofDual b +ᵥ a = b +ᵥ a
<VAR>α : Type u_1<VAR>One α<GOAL>toLex 1 = 1
<VAR>α : Type u_1<VAR>Zero α<GOAL>toLex 0 = 0
<VAR>α : Type u_1<VAR>One α<GOAL>ofLex 1 = 1
<VAR>α : Type u_1<VAR>Zero α<GOAL>ofLex 0 = 0
<VAR>α : Type u_1<VAR>Add α<VAR>a b : α<GOAL>toLex (a + b) = toLex a + toLex b
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : α<GOAL>toLex (a * b) = toLex a * toLex b
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : Lex α<GOAL>ofLex (a * b) = ofLex a * ofLex b
<VAR>α : Type u_1<VAR>Add α<VAR>a b : Lex α<GOAL>ofLex (a + b) = ofLex a + ofLex b
<VAR>α : Type u_1<VAR>Inv α<VAR>a : α<GOAL>toLex a⁻¹ = (toLex a)⁻¹
<VAR>α : Type u_1<VAR>Neg α<VAR>a : α<GOAL>toLex (-a) = -toLex a
<VAR>α : Type u_1<VAR>Neg α<VAR>a : Lex α<GOAL>ofLex (-a) = -ofLex a
<VAR>α : Type u_1<VAR>Inv α<VAR>a : Lex α<GOAL>ofLex a⁻¹ = (ofLex a)⁻¹
<VAR>α : Type u_1<VAR>Div α<VAR>a b : α<GOAL>toLex (a / b) = toLex a / toLex b
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : α<GOAL>toLex (a - b) = toLex a - toLex b
<VAR>α : Type u_1<VAR>Sub α<VAR>a b : Lex α<GOAL>ofLex (a - b) = ofLex a - ofLex b
<VAR>α : Type u_1<VAR>Div α<VAR>a b : Lex α<GOAL>ofLex (a / b) = ofLex a / ofLex b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : α<VAR>b : β<GOAL>toLex (a ^ b) = toLex a ^ b
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : β<VAR>a : α<GOAL>toLex (b • a) = b • toLex a
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : β<VAR>a : α<GOAL>toLex (b +ᵥ a) = b +ᵥ toLex a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : Lex α<VAR>b : β<GOAL>ofLex (a ^ b) = ofLex a ^ b
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : β<VAR>a : Lex α<GOAL>ofLex (b • a) = b • ofLex a
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : β<VAR>a : Lex α<GOAL>ofLex (b +ᵥ a) = b +ᵥ ofLex a
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : β<VAR>a : α<GOAL>toLex b • a = b • a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : α<VAR>b : β<GOAL>a ^ toLex b = a ^ b
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : β<VAR>a : α<GOAL>toLex b +ᵥ a = b +ᵥ a
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>VAdd β α<VAR>b : Lex β<VAR>a : α<GOAL>ofLex b +ᵥ a = b +ᵥ a
<VAR>β : Type u_2<VAR>α : Type u_1<VAR>SMul β α<VAR>b : Lex β<VAR>a : α<GOAL>ofLex b • a = b • a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Pow α β<VAR>a : α<VAR>b : Lex β<GOAL>a ^ ofLex b = a ^ b
<VAR>α : Type u_1<VAR>AddGroupWithOne α<VAR>n : ℤ<GOAL>↑n.natAbs = ↑|n|
<VAR>α : Type u_1<VAR>AddCommGroupWithOne α<VAR>m n : ℤ<GOAL>↑(m * n) = m • ↑n
<VAR>m : ℤ<VAR>even : Even m<GOAL>2 ≤ m ↔ 0 < m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>self : PosSMulMono α β<VAR>a : α<VAR>ha : 0 ≤ a<VAR>b₁ b₂ : β<VAR>hb : b₁ ≤ b₂<GOAL>a • b₁ ≤ a • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>self : PosSMulStrictMono α β<VAR>a : α<VAR>ha : 0 < a<VAR>b₁ b₂ : β<VAR>hb : b₁ < b₂<GOAL>a • b₁ < a • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>self : PosSMulReflectLT α β<VAR>a : α<VAR>ha : 0 ≤ a<VAR>b₁ b₂ : β<VAR>hb : a • b₁ < a • b₂<GOAL>b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>self : PosSMulReflectLE α β<VAR>a : α<VAR>ha : 0 < a<VAR>b₁ b₂ : β<VAR>hb : a • b₁ ≤ a • b₂<GOAL>b₁ ≤ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>self : SMulPosMono α β<VAR>b : β<VAR>hb : 0 ≤ b<VAR>a₁ a₂ : α<VAR>ha : a₁ ≤ a₂<GOAL>a₁ • b ≤ a₂ • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>self : SMulPosStrictMono α β<VAR>b : β<VAR>hb : 0 < b<VAR>a₁ a₂ : α<VAR>ha : a₁ < a₂<GOAL>a₁ • b < a₂ • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>self : SMulPosReflectLT α β<VAR>b : β<VAR>hb : 0 ≤ b<VAR>a₁ a₂ : α<GOAL>a₁ • b < a₂ • b → a₁ < a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>self : SMulPosReflectLE α β<VAR>b : β<VAR>hb : 0 < b<VAR>a₁ a₂ : α<GOAL>a₁ • b ≤ a₂ • b → a₁ ≤ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>ha : 0 ≤ a<GOAL>Monotone fun x => a • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulStrictMono α β<VAR>ha : 0 < a<GOAL>StrictMono fun x => a • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>hb : b₁ ≤ b₂<VAR>ha : 0 ≤ a<GOAL>a • b₁ ≤ a • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulStrictMono α β<VAR>hb : b₁ < b₂<VAR>ha : 0 < a<GOAL>a • b₁ < a • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulReflectLT α β<VAR>h : a • b₁ < a • b₂<VAR>ha : 0 ≤ a<GOAL>b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulReflectLE α β<VAR>h : a • b₁ ≤ a • b₂<VAR>ha : 0 < a<GOAL>b₁ ≤ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>ha : 0 < a<GOAL>a • b₁ ≤ a • b₂ ↔ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>PosSMulStrictMono α β<VAR>PosSMulReflectLT α β<VAR>ha : 0 < a<GOAL>a • b₁ < a • b₂ ↔ b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosMono α β<VAR>hb : 0 ≤ b<GOAL>Monotone fun x => x • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosStrictMono α β<VAR>hb : 0 < b<GOAL>StrictMono fun x => x • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : 0 ≤ b<GOAL>a₁ • b ≤ a₂ • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosStrictMono α β<VAR>ha : a₁ < a₂<VAR>hb : 0 < b<GOAL>a₁ • b < a₂ • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosReflectLT α β<VAR>h : a₁ • b < a₂ • b<VAR>hb : 0 ≤ b<GOAL>a₁ < a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosReflectLE α β<VAR>h : a₁ • b ≤ a₂ • b<VAR>hb : 0 < b<GOAL>a₁ ≤ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosMono α β<VAR>SMulPosReflectLE α β<VAR>hb : 0 < b<GOAL>a₁ • b ≤ a₂ • b ↔ a₁ ≤ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosStrictMono α β<VAR>SMulPosReflectLT α β<VAR>hb : 0 < b<GOAL>a₁ • b < a₂ • b ↔ a₁ < a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>Zero β<VAR>PosSMulStrictMono α β<VAR>SMulPosMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ < b₂<VAR>h₁ : 0 < a₁<VAR>h₂ : 0 ≤ b₂<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>Zero β<VAR>PosSMulStrictMono α β<VAR>SMulPosMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ < b₂<VAR>h₂ : 0 < a₂<VAR>h₁ : 0 ≤ b₁<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>Zero β<VAR>PosSMulMono α β<VAR>SMulPosStrictMono α β<VAR>ha : a₁ < a₂<VAR>hb : b₁ ≤ b₂<VAR>h₁ : 0 ≤ a₁<VAR>h₂ : 0 < b₂<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>Zero β<VAR>PosSMulMono α β<VAR>SMulPosStrictMono α β<VAR>ha : a₁ < a₂<VAR>hb : b₁ ≤ b₂<VAR>h₂ : 0 ≤ a₂<VAR>h₁ : 0 < b₁<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>Zero β<VAR>PosSMulStrictMono α β<VAR>SMulPosStrictMono α β<VAR>ha : a₁ < a₂<VAR>hb : b₁ < b₂<VAR>h₁ : 0 < a₁<VAR>h₂ : 0 < b₂<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>Zero β<VAR>PosSMulStrictMono α β<VAR>SMulPosStrictMono α β<VAR>ha : a₁ < a₂<VAR>hb : b₁ < b₂<VAR>h₂ : 0 < a₂<VAR>h₁ : 0 < b₁<GOAL>a₁ • b₁ < a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>Zero β<VAR>PosSMulMono α β<VAR>SMulPosMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₁ : 0 ≤ a₁<VAR>h₂ : 0 ≤ b₂<GOAL>a₁ • b₁ ≤ a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>SMul α β<VAR>Preorder α<VAR>Preorder β<VAR>Zero α<VAR>Zero β<VAR>PosSMulMono α β<VAR>SMulPosMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₂ : 0 ≤ a₂<VAR>h₁ : 0 ≤ b₁<GOAL>a₁ • b₁ ≤ a₂ • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>LinearOrder β<VAR>Zero α<VAR>PosSMulReflectLE α β<GOAL>PosSMulStrictMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>LinearOrder β<VAR>Zero α<GOAL>PosSMulStrictMono α β ↔ PosSMulReflectLE α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>LinearOrder β<VAR>Zero α<VAR>PosSMulReflectLT α β<GOAL>PosSMulMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>LinearOrder β<VAR>Zero α<GOAL>PosSMulMono α β ↔ PosSMulReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>SMul α β<VAR>Preorder α<VAR>LinearOrder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>ha : 0 ≤ a<VAR>b₁ b₂ : β<GOAL>a • max b₁ b₂ = max (a • b₁) (a • b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>SMul α β<VAR>Preorder α<VAR>LinearOrder β<VAR>Zero α<VAR>PosSMulMono α β<VAR>ha : 0 ≤ a<VAR>b₁ b₂ : β<GOAL>a • min b₁ b₂ = min (a • b₁) (a • b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>LinearOrder β<VAR>Zero β<VAR>SMulPosReflectLE α β<GOAL>SMulPosStrictMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>Preorder α<VAR>LinearOrder β<VAR>Zero β<VAR>SMulPosReflectLT α β<GOAL>SMulPosMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>LinearOrder α<VAR>Preorder β<VAR>Zero β<VAR>SMulPosMono α β<GOAL>SMulPosReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>LinearOrder α<VAR>LinearOrder β<VAR>Zero β<GOAL>SMulPosStrictMono α β ↔ SMulPosReflectLE α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>SMul α β<VAR>LinearOrder α<VAR>LinearOrder β<VAR>Zero β<GOAL>SMulPosMono α β ↔ SMulPosReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulStrictMono α β<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulStrictMono α β<VAR>ha : 0 < a<VAR>hb : b < 0<GOAL>a • b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulStrictMono α β<VAR>PosSMulReflectLT α β<VAR>ha : 0 < a<GOAL>0 < a • b ↔ 0 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulStrictMono α β<VAR>PosSMulReflectLT α β<VAR>ha : 0 < a<GOAL>a • b < 0 ↔ b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ : β<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulMono α β<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b₁<GOAL>0 ≤ a • b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulMono α β<VAR>ha : 0 ≤ a<VAR>hb : b ≤ 0<GOAL>a • b ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulReflectLT α β<VAR>h : 0 < a • b<VAR>ha : 0 ≤ a<GOAL>0 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulZeroClass α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulReflectLT α β<VAR>h : a • b < 0<VAR>ha : 0 ≤ a<GOAL>b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosStrictMono α β<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosStrictMono α β<VAR>ha : a < 0<VAR>hb : 0 < b<GOAL>a • b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosStrictMono α β<VAR>SMulPosReflectLT α β<VAR>hb : 0 < b<GOAL>0 < a • b ↔ 0 < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosMono α β<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b₁<GOAL>0 ≤ a • b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosMono α β<VAR>ha : a ≤ 0<VAR>hb : 0 ≤ b<GOAL>a • b ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosReflectLT α β<VAR>h : 0 < a • b<VAR>hb : 0 ≤ b<GOAL>0 < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosReflectLT α β<VAR>h : a • b < 0<VAR>hb : 0 ≤ b<GOAL>a < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>Preorder β<VAR>PosSMulReflectLT α β<VAR>SMulPosReflectLT α β<VAR>hab : 0 < a • b<GOAL>0 < a ↔ 0 < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>PartialOrder α<VAR>Preorder β<VAR>h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂<GOAL>PosSMulMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>PartialOrder α<VAR>Preorder β<VAR>h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂<GOAL>PosSMulReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>PartialOrder β<VAR>h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b<GOAL>SMulPosMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>Preorder α<VAR>PartialOrder β<VAR>h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂<GOAL>SMulPosReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>PartialOrder α<VAR>PartialOrder β<VAR>PosSMulStrictMono α β<VAR>SMulPosStrictMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₁ : 0 < a₁<VAR>h₂ : 0 < b₂<GOAL>a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>PartialOrder α<VAR>PartialOrder β<VAR>PosSMulStrictMono α β<VAR>SMulPosStrictMono α β<VAR>ha : a₁ ≤ a₂<VAR>hb : b₁ ≤ b₂<VAR>h₂ : 0 < a₂<VAR>h₁ : 0 < b₁<GOAL>a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>LinearOrder α<VAR>LinearOrder β<VAR>PosSMulMono α β<VAR>SMulPosMono α β<VAR>hab : 0 < a • b<GOAL>0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>LinearOrder α<VAR>LinearOrder β<VAR>PosSMulMono α β<VAR>SMulPosMono α β<VAR>h : 0 < a • b<VAR>ha : a ≤ 0<GOAL>b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>LinearOrder α<VAR>LinearOrder β<VAR>PosSMulMono α β<VAR>SMulPosMono α β<VAR>h : 0 < a • b<VAR>ha : b ≤ 0<GOAL>a < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>LinearOrder α<VAR>LinearOrder β<VAR>PosSMulMono α β<VAR>SMulPosMono α β<VAR>hab : 0 < a • b<GOAL>a < 0 ↔ b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>LinearOrder α<VAR>LinearOrder β<VAR>SMulPosMono α β<VAR>h : a • b < 0<VAR>ha : 0 ≤ a<GOAL>b < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>LinearOrder α<VAR>LinearOrder β<VAR>PosSMulMono α β<VAR>h : a • b < 0<VAR>hb : 0 ≤ b<GOAL>a < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Monoid α<VAR>Zero β<VAR>MulAction α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosMono α β<VAR>SMulPosReflectLE α β<VAR>hb : 0 < b<GOAL>b ≤ a • b ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Monoid α<VAR>Zero β<VAR>MulAction α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosStrictMono α β<VAR>SMulPosReflectLT α β<VAR>hb : 0 < b<GOAL>b < a • b ↔ 1 < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Monoid α<VAR>Zero β<VAR>MulAction α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosMono α β<VAR>SMulPosReflectLE α β<VAR>hb : 0 < b<GOAL>a • b ≤ b ↔ a ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Monoid α<VAR>Zero β<VAR>MulAction α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosStrictMono α β<VAR>SMulPosReflectLT α β<VAR>hb : 0 < b<GOAL>a • b < b ↔ a < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Monoid α<VAR>Zero β<VAR>MulAction α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosMono α β<VAR>hb : 0 ≤ b<VAR>h : a ≤ 1<GOAL>a • b ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Monoid α<VAR>Zero β<VAR>MulAction α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosMono α β<VAR>hb : 0 ≤ b<VAR>h : 1 ≤ a<GOAL>b ≤ a • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Monoid α<VAR>Zero β<VAR>MulAction α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosStrictMono α β<VAR>hb : 0 < b<VAR>h : a < 1<GOAL>a • b < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>Monoid α<VAR>Zero β<VAR>MulAction α β<VAR>Preorder α<VAR>Preorder β<VAR>SMulPosStrictMono α β<VAR>hb : 0 < b<VAR>h : 1 < a<GOAL>b < a • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Semiring α<VAR>AddCommGroup β<VAR>Module α β<VAR>NoZeroSMulDivisors α β<VAR>Preorder α<VAR>PartialOrder β<VAR>PosSMulMono α β<GOAL>PosSMulStrictMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Semiring α<VAR>AddCommGroup β<VAR>Module α β<VAR>NoZeroSMulDivisors α β<VAR>PartialOrder α<VAR>PartialOrder β<GOAL>PosSMulMono α β ↔ PosSMulStrictMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Semiring α<VAR>AddCommGroup β<VAR>Module α β<VAR>NoZeroSMulDivisors α β<VAR>PartialOrder α<VAR>PartialOrder β<GOAL>PosSMulReflectLE α β ↔ PosSMulReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ring α<VAR>AddCommGroup β<VAR>Module α β<VAR>NoZeroSMulDivisors α β<VAR>PartialOrder α<VAR>PartialOrder β<VAR>SMulPosMono α β<GOAL>SMulPosStrictMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ring α<VAR>AddCommGroup β<VAR>Module α β<VAR>NoZeroSMulDivisors α β<VAR>PartialOrder α<VAR>PartialOrder β<GOAL>SMulPosMono α β ↔ SMulPosStrictMono α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ring α<VAR>AddCommGroup β<VAR>Module α β<VAR>NoZeroSMulDivisors α β<VAR>PartialOrder α<VAR>PartialOrder β<VAR>SMulPosReflectLT α β<GOAL>SMulPosReflectLE α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ring α<VAR>AddCommGroup β<VAR>Module α β<VAR>NoZeroSMulDivisors α β<VAR>PartialOrder α<VAR>PartialOrder β<GOAL>SMulPosReflectLE α β ↔ SMulPosReflectLT α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>GroupWithZero α<VAR>Preorder α<VAR>Preorder β<VAR>MulAction α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>ha : 0 < a<GOAL>a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>GroupWithZero α<VAR>Preorder α<VAR>Preorder β<VAR>MulAction α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>ha : 0 < a<GOAL>b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>GroupWithZero α<VAR>Preorder α<VAR>Preorder β<VAR>MulAction α β<VAR>PosSMulStrictMono α β<VAR>PosSMulReflectLT α β<VAR>ha : 0 < a<GOAL>a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b₁ b₂ : β<VAR>GroupWithZero α<VAR>Preorder α<VAR>Preorder β<VAR>MulAction α β<VAR>PosSMulStrictMono α β<VAR>PosSMulReflectLT α β<VAR>ha : 0 < a<GOAL>b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>GroupWithZero α<VAR>Preorder α<VAR>Preorder β<VAR>MulAction α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>a : α<VAR>ha : 0 < a<VAR>b : β<GOAL>(RelIso.symm (OrderIso.smulRight ha)) b = a⁻¹ • b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>GroupWithZero α<VAR>Preorder α<VAR>Preorder β<VAR>MulAction α β<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>a : α<VAR>ha : 0 < a<VAR>b : β<GOAL>(OrderIso.smulRight ha) b = a • b