ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : Set α<VAR>a : α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (a • s)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : Set α<VAR>a : α<VAR>hs : IsLowerSet s<GOAL>IsLowerSet (a • s)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : Set α<VAR>a : α<VAR>hs : IsLowerSet s<GOAL>IsLowerSet (a +ᵥ s)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : Set α<VAR>a : α<VAR>hs : s.OrdConnected<GOAL>(a +ᵥ s).OrdConnected
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : Set α<VAR>a : α<VAR>hs : s.OrdConnected<GOAL>(a • s).OrdConnected
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<VAR>ht : IsUpperSet t<GOAL>IsUpperSet (s + t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<VAR>ht : IsUpperSet t<GOAL>IsUpperSet (s * t)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (s + t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (s * t)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<VAR>ht : IsLowerSet t<GOAL>IsLowerSet (s + t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<VAR>ht : IsLowerSet t<GOAL>IsLowerSet (s * t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<VAR>hs : IsLowerSet s<GOAL>IsLowerSet (s * t)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<VAR>hs : IsLowerSet s<GOAL>IsLowerSet (s + t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>IsLowerSet s⁻¹
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>IsLowerSet (-s)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>IsUpperSet (-s)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>IsUpperSet s⁻¹
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<VAR>ht : IsUpperSet t<GOAL>IsLowerSet (s / t)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<VAR>ht : IsUpperSet t<GOAL>IsLowerSet (s - t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (s / t)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (s - t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<VAR>ht : IsLowerSet t<GOAL>IsUpperSet (s / t)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<VAR>ht : IsLowerSet t<GOAL>IsUpperSet (s - t)
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<VAR>hs : IsLowerSet s<GOAL>IsLowerSet (s - t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<VAR>hs : IsLowerSet s<GOAL>IsLowerSet (s / t)
<VAR>α : Type u_1<VAR>OrderedCommGroup α<GOAL>↑1 = Set.Ici 1
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<GOAL>↑0 = Set.Ici 0
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : UpperSet α<GOAL>↑(s * t) = ↑s * ↑t
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : UpperSet α<GOAL>↑(s + t) = ↑s + ↑t
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : UpperSet α<GOAL>↑(s / t) = ↑s / ↑t
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : UpperSet α<GOAL>↑(s - t) = ↑s - ↑t
<VAR>α : Type u_1<VAR>OrderedCommGroup α<GOAL>UpperSet.Ici 1 = 1
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<GOAL>UpperSet.Ici 0 = 0
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : UpperSet α<GOAL>0 + s = s
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : UpperSet α<GOAL>1 * s = s
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : LowerSet α<GOAL>↑(s * t) = ↑s * ↑t
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : LowerSet α<GOAL>↑(s + t) = ↑s + ↑t
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : LowerSet α<GOAL>↑(s - t) = ↑s - ↑t
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : LowerSet α<GOAL>↑(s / t) = ↑s / ↑t
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<GOAL>LowerSet.Iic 0 = 0
<VAR>α : Type u_1<VAR>OrderedCommGroup α<GOAL>LowerSet.Iic 1 = 1
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : LowerSet α<GOAL>1 * s = s
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : LowerSet α<GOAL>0 + s = s
<VAR>α : Type u_1<VAR>OrderedCommGroup α<GOAL>upperClosure 1 = 1
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<GOAL>upperClosure 0 = 0
<VAR>α : Type u_1<VAR>OrderedCommGroup α<GOAL>lowerClosure 1 = 1
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<GOAL>lowerClosure 0 = 0
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : Set α<VAR>a : α<GOAL>upperClosure (a +ᵥ s) = a +ᵥ upperClosure s
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : Set α<VAR>a : α<GOAL>upperClosure (a • s) = a • upperClosure s
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s : Set α<VAR>a : α<GOAL>lowerClosure (a • s) = a • lowerClosure s
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s : Set α<VAR>a : α<GOAL>lowerClosure (a +ᵥ s) = a +ᵥ lowerClosure s
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<GOAL>s * ↑(upperClosure t) = ↑(upperClosure (s * t))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<GOAL>s + ↑(upperClosure t) = ↑(upperClosure (s + t))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<GOAL>s + ↑(lowerClosure t) = ↑(lowerClosure (s + t))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<GOAL>s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<GOAL>↑(upperClosure s) + t = ↑(upperClosure (s + t))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<GOAL>↑(upperClosure s) * t = ↑(upperClosure (s * t))
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<GOAL>↑(lowerClosure s) + t = ↑(lowerClosure (s + t))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<GOAL>↑(lowerClosure s) * t = ↑(lowerClosure (s * t))
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<GOAL>upperClosure (s * t) = upperClosure s * upperClosure t
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<GOAL>upperClosure (s + t) = upperClosure s + upperClosure t
<VAR>α : Type u_1<VAR>OrderedCommGroup α<VAR>s t : Set α<GOAL>lowerClosure (s * t) = lowerClosure s * lowerClosure t
<VAR>α : Type u_1<VAR>OrderedAddCommGroup α<VAR>s t : Set α<GOAL>lowerClosure (s + t) = lowerClosure s + lowerClosure t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>self : FloorDiv α β<VAR>a : α<GOAL>0 < a → GaloisConnection (fun x => a • x) fun x => x ⌊/⌋ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>self : FloorDiv α β<VAR>a : α<GOAL>a ≤ 0 → ∀ (b : β), b ⌊/⌋ a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>self : FloorDiv α β<VAR>a : α<GOAL>0 ⌊/⌋ a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>self : CeilDiv α β<VAR>a : α<GOAL>a ≤ 0 → ∀ (b : β), b ⌈/⌉ a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>self : CeilDiv α β<VAR>a : α<GOAL>0 < a → GaloisConnection (fun x => x ⌈/⌉ a) fun x => a • x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>self : CeilDiv α β<VAR>a : α<GOAL>0 ⌈/⌉ a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>a : α<VAR>ha : 0 < a<GOAL>GaloisConnection (fun x => a • x) fun x => x ⌊/⌋ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>a : α<VAR>b c : β<VAR>ha : 0 < a<GOAL>c ≤ b ⌊/⌋ a ↔ a • c ≤ b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>a : α<VAR>ha : a ≤ 0<VAR>b : β<GOAL>b ⌊/⌋ a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>b : β<GOAL>b ⌊/⌋ 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>a : α<GOAL>0 ⌊/⌋ a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>a : α<VAR>b : β<VAR>ha : 0 < a<GOAL>a • (b ⌊/⌋ a) ≤ b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>a : α<VAR>ha : 0 < a<GOAL>GaloisConnection (fun x => x ⌈/⌉ a) fun x => a • x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>a : α<VAR>b c : β<VAR>ha : 0 < a<GOAL>b ⌈/⌉ a ≤ c ↔ b ≤ a • c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>a : α<VAR>ha : a ≤ 0<VAR>b : β<GOAL>b ⌈/⌉ a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>b : β<GOAL>b ⌈/⌉ 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>a : α<GOAL>0 ⌈/⌉ a = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>a : α<VAR>b : β<VAR>ha : 0 < a<GOAL>b ≤ a • (b ⌈/⌉ a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>PosSMulReflectLE α β<VAR>FloorDiv α β<VAR>CeilDiv α β<VAR>a : α<VAR>b : β<GOAL>b ⌊/⌋ a ≤ b ⌈/⌉ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedAddCommMonoid β<VAR>MulActionWithZero α β<VAR>FloorDiv α β<VAR>Nontrivial α<VAR>b : β<GOAL>b ⌊/⌋ 1 = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedAddCommMonoid β<VAR>MulActionWithZero α β<VAR>FloorDiv α β<VAR>a : α<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>ha : 0 < a<VAR>b : β<GOAL>a • b ⌊/⌋ a = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedAddCommMonoid β<VAR>MulActionWithZero α β<VAR>CeilDiv α β<VAR>Nontrivial α<VAR>b : β<GOAL>b ⌈/⌉ 1 = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedSemiring α<VAR>OrderedAddCommMonoid β<VAR>MulActionWithZero α β<VAR>CeilDiv α β<VAR>a : α<VAR>PosSMulMono α β<VAR>PosSMulReflectLE α β<VAR>ha : 0 < a<VAR>b : β<GOAL>a • b ⌈/⌉ a = b
<VAR>α : Type u_2<VAR>OrderedSemiring α<VAR>FloorDiv α α<VAR>a : α<VAR>ha : 0 < a<GOAL>GaloisConnection (fun x => a * x) fun x => x ⌊/⌋ a
<VAR>α : Type u_2<VAR>OrderedSemiring α<VAR>FloorDiv α α<VAR>a b c : α<VAR>ha : 0 < a<GOAL>c ≤ b ⌊/⌋ a ↔ a • c ≤ b
<VAR>α : Type u_2<VAR>OrderedSemiring α<VAR>CeilDiv α α<VAR>a : α<VAR>ha : 0 < a<GOAL>GaloisConnection (fun x => x ⌈/⌉ a) fun x => a * x
<VAR>α : Type u_2<VAR>OrderedSemiring α<VAR>CeilDiv α α<VAR>a b c : α<VAR>ha : 0 < a<GOAL>b ⌈/⌉ a ≤ c ↔ b ≤ a * c
<VAR>a b : ℕ<GOAL>a ⌊/⌋ b = a / b
<VAR>a b : ℕ<GOAL>a ⌈/⌉ b = (a + b - 1) / b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>π : ι → Type u_4<VAR>OrderedAddCommMonoid α<VAR>(i : ι) → OrderedAddCommMonoid (π i)<VAR>(i : ι) → SMulZeroClass α (π i)<VAR>(i : ι) → FloorDiv α (π i)<VAR>f : (i : ι) → π i<VAR>a : α<GOAL>f ⌊/⌋ a = fun i => f i ⌊/⌋ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>π : ι → Type u_4<VAR>OrderedAddCommMonoid α<VAR>(i : ι) → OrderedAddCommMonoid (π i)<VAR>(i : ι) → SMulZeroClass α (π i)<VAR>(i : ι) → FloorDiv α (π i)<VAR>f : (i : ι) → π i<VAR>a : α<VAR>i : ι<GOAL>(f ⌊/⌋ a) i = f i ⌊/⌋ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>π : ι → Type u_4<VAR>OrderedAddCommMonoid α<VAR>(i : ι) → OrderedAddCommMonoid (π i)<VAR>(i : ι) → SMulZeroClass α (π i)<VAR>(i : ι) → CeilDiv α (π i)<VAR>f : (i : ι) → π i<VAR>a : α<GOAL>f ⌈/⌉ a = fun i => f i ⌈/⌉ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>π : ι → Type u_4<VAR>OrderedAddCommMonoid α<VAR>(i : ι) → OrderedAddCommMonoid (π i)<VAR>(i : ι) → SMulZeroClass α (π i)<VAR>(i : ι) → CeilDiv α (π i)<VAR>f : (i : ι) → π i<VAR>a : α<VAR>i : ι<GOAL>(f ⌈/⌉ a) i = f i ⌈/⌉ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>f : ι →₀ β<VAR>a : α<GOAL>f ⌊/⌋ a = Finsupp.mapRange (fun x => x ⌊/⌋ a) ⋯ f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>f : ι →₀ β<VAR>a : α<GOAL>⇑(f ⌊/⌋ a) = fun i => f i ⌊/⌋ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>f : ι →₀ β<VAR>a : α<VAR>i : ι<GOAL>(f ⌊/⌋ a) i = f i ⌊/⌋ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>FloorDiv α β<VAR>f : ι →₀ β<VAR>a : α<GOAL>(f ⌊/⌋ a).support ⊆ f.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>f : ι →₀ β<VAR>a : α<GOAL>f ⌈/⌉ a = Finsupp.mapRange (fun x => x ⌈/⌉ a) ⋯ f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>f : ι →₀ β<VAR>a : α<GOAL>⇑(f ⌈/⌉ a) = fun i => f i ⌈/⌉ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>f : ι →₀ β<VAR>a : α<VAR>i : ι<GOAL>(f ⌈/⌉ a) i = f i ⌈/⌉ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>OrderedAddCommMonoid α<VAR>OrderedAddCommMonoid β<VAR>SMulZeroClass α β<VAR>CeilDiv α β<VAR>f : ι →₀ β<VAR>a : α<GOAL>(f ⌈/⌉ a).support ⊆ f.support
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>DistribMulAction ℚ≥0 α<VAR>PosSMulMono ℚ≥0 α<VAR>q : ℚ≥0<VAR>a : α<GOAL>|q • a| = q • |a|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>Module ℚ α<VAR>PosSMulMono ℚ α<VAR>q : ℚ<VAR>a : α<GOAL>|q • a| = |q| • |a|
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>a₁ a₂ : α<VAR>h : a₁ ≤ a₂<GOAL>LinearOrderedField.cutMap β a₁ ⊆ LinearOrderedField.cutMap β a₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>a : α<VAR>b : β<GOAL>b ∈ LinearOrderedField.cutMap β a ↔ ∃ q, ↑q < a ∧ ↑q = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>a : α<VAR>q : ℚ<VAR>CharZero β<GOAL>↑q ∈ LinearOrderedField.cutMap β a ↔ ↑q < a
<VAR>α : Type u_2<VAR>LinearOrderedField α<VAR>a : α<GOAL>LinearOrderedField.cutMap α a = Set.Iio a ∩ Set.range Rat.cast
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>LinearOrderedField β<VAR>q : ℚ<GOAL>LinearOrderedField.cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>LinearOrderedField β<VAR>Archimedean α<VAR>a : α<GOAL>(LinearOrderedField.cutMap β a).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>LinearOrderedField β<VAR>Archimedean α<VAR>a : α<GOAL>BddAbove (LinearOrderedField.cutMap β a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>LinearOrderedField β<VAR>Archimedean α<VAR>a b : α<GOAL>LinearOrderedField.cutMap β (a + b) = LinearOrderedField.cutMap β a + LinearOrderedField.cutMap β b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<GOAL>Monotone (LinearOrderedField.inducedMap α β)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<VAR>q : ℚ<GOAL>LinearOrderedField.inducedMap α β ↑q = ↑q
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<GOAL>LinearOrderedField.inducedMap α β 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<GOAL>LinearOrderedField.inducedMap α β 1 = 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ LinearOrderedField.inducedMap α β a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<VAR>a : α<VAR>q : ℚ<GOAL>↑q < LinearOrderedField.inducedMap α β a ↔ ↑q < a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<VAR>a : α<VAR>b : β<GOAL>b < LinearOrderedField.inducedMap α β a ↔ ∃ q, b < ↑q ∧ ↑q < a
<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrderedField β<VAR>b : β<GOAL>LinearOrderedField.inducedMap β β b = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>ConditionallyCompleteLinearOrderedField γ<VAR>Archimedean α<VAR>a : α<GOAL>LinearOrderedField.inducedMap β γ (LinearOrderedField.inducedMap α β a) = LinearOrderedField.inducedMap α γ a
<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ConditionallyCompleteLinearOrderedField β<VAR>ConditionallyCompleteLinearOrderedField γ<VAR>b : β<GOAL>LinearOrderedField.inducedMap γ β (LinearOrderedField.inducedMap β γ b) = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<VAR>x y : α<GOAL>LinearOrderedField.inducedMap α β (x + y) = LinearOrderedField.inducedMap α β x + LinearOrderedField.inducedMap α β y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b : β<VAR>hb : b ∈ LinearOrderedField.cutMap β (a * a)<GOAL>b ≤ LinearOrderedField.inducedMap α β a * LinearOrderedField.inducedMap α β a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b : β<VAR>hba : b < LinearOrderedField.inducedMap α β a * LinearOrderedField.inducedMap α β a<GOAL>∃ c ∈ LinearOrderedField.cutMap β (a * a), b < c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedField α<VAR>ConditionallyCompleteLinearOrderedField β<VAR>Archimedean α<GOAL>∀ (a : α), (LinearOrderedField.inducedOrderRingHom α β) a = (LinearOrderedField.inducedAddHom α β) a
<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ConditionallyCompleteLinearOrderedField β<VAR>ConditionallyCompleteLinearOrderedField γ<GOAL>⇑(LinearOrderedField.inducedOrderRingIso β γ) = LinearOrderedField.inducedMap β γ
<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ConditionallyCompleteLinearOrderedField β<VAR>ConditionallyCompleteLinearOrderedField γ<GOAL>(LinearOrderedField.inducedOrderRingIso β γ).symm = LinearOrderedField.inducedOrderRingIso γ β
<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrderedField β<GOAL>LinearOrderedField.inducedOrderRingIso β β = OrderRingIso.refl β
<VAR>R : Type u_5<VAR>S : Type u_6<VAR>OrderedRing R<VAR>LinearOrderedRing S<VAR>hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r<VAR>f : R →+* S<GOAL>Monotone ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Add α<VAR>Sub α<VAR>OrderedSub α<VAR>Preorder β<VAR>Add β<VAR>Sub β<VAR>OrderedSub β<VAR>f : AddHom α β<VAR>hf : Monotone ⇑f<VAR>a b : α<GOAL>f a - f b ≤ f (a - b)
<VAR>R : Type u_3<VAR>Distrib R<VAR>Preorder R<VAR>Sub R<VAR>OrderedSub R<VAR>CovariantClass R R (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : R<GOAL>a * b - a * c ≤ a * (b - c)
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Preorder R<VAR>Sub R<VAR>OrderedSub R<VAR>CovariantClass R R (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : R<GOAL>a * c - b * c ≤ (a - b) * c
<VAR>M : Type u_3<VAR>N : Type u_4<VAR>Preorder M<VAR>Add M<VAR>Sub M<VAR>OrderedSub M<VAR>PartialOrder N<VAR>Add N<VAR>Sub N<VAR>OrderedSub N<VAR>e : M ≃o N<VAR>h_add : ∀ (a b : M), e (a + b) = e a + e b<VAR>a b : M<GOAL>e (a - b) = e a - e b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>AddCommMonoid α<VAR>Sub α<VAR>OrderedSub α<VAR>Preorder β<VAR>AddCommMonoid β<VAR>Sub β<VAR>OrderedSub β<VAR>f : α →+ β<VAR>hf : Monotone ⇑f<VAR>a b : α<GOAL>f a - f b ≤ f (a - b)
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>hnezero : Polynomial.derivative p ≠ 0<GOAL>Polynomial.rootMultiplicity t p - 1 ≤ Polynomial.rootMultiplicity t (Polynomial.derivative p)
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>hpt : p.IsRoot t<VAR>hnzd : ↑(Polynomial.rootMultiplicity t p) ∈ nonZeroDivisors R<GOAL>Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>hn : n < Polynomial.rootMultiplicity t p<GOAL>((⇑Polynomial.derivative)^[n] p).IsRoot t
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<GOAL>Polynomial.eval t ((⇑Polynomial.derivative)^[Polynomial.rootMultiplicity t p] p) = (Polynomial.rootMultiplicity t p).factorial • Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p)
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t<VAR>hnzd : ↑n.factorial ∈ nonZeroDivisors R<GOAL>n < Polynomial.rootMultiplicity t p
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t<VAR>hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R<GOAL>n < Polynomial.rootMultiplicity t p
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hnzd : ↑n.factorial ∈ nonZeroDivisors R<GOAL>n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R<GOAL>n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>h : p ≠ 0<GOAL>1 < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ 1, ((⇑Polynomial.derivative)^[m] p).IsRoot t
<VAR>R : Type u<VAR>CommRing R<VAR>p : R[X]<VAR>t : R<VAR>h : p ≠ 0<GOAL>1 < Polynomial.rootMultiplicity t p ↔ p.IsRoot t ∧ (Polynomial.derivative p).IsRoot t
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>GCDMonoid R[X]<VAR>p : R[X]<VAR>t : R<VAR>h : p ≠ 0<GOAL>1 < Polynomial.rootMultiplicity t p ↔ (gcd p (Polynomial.derivative p)).IsRoot t
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>CharZero R<VAR>p : R[X]<VAR>t : R<VAR>hpt : p.IsRoot t<GOAL>Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>CharZero R<VAR>p : R[X]<VAR>t : R<GOAL>Polynomial.rootMultiplicity t p - 1 ≤ Polynomial.rootMultiplicity t (Polynomial.derivative p)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>CharZero R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<VAR>hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t<GOAL>n < Polynomial.rootMultiplicity t p
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>CharZero R<VAR>p : R[X]<VAR>t : R<VAR>n : ℕ<VAR>h : p ≠ 0<GOAL>n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizationMonoid R<VAR>p : R[X]<GOAL>↑(normUnit p) = Polynomial.C ↑(normUnit p.leadingCoeff)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizationMonoid R<VAR>p : R[X]<GOAL>(normalize p).leadingCoeff = normalize p.leadingCoeff
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizationMonoid R<VAR>p : R[X]<VAR>hp : p.Monic<GOAL>normalize p = p
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizationMonoid R<VAR>p : R[X]<GOAL>(normalize p).roots = p.roots
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizationMonoid R<GOAL>normUnit Polynomial.X = 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizationMonoid R<GOAL>Polynomial.X = normalize Polynomial.X
<VAR>R : Type u<VAR>DivisionRing R<VAR>p : R[X]<VAR>hp0 : p ≠ 0<VAR>hp : ¬IsUnit p<GOAL>0 < p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>DivisionRing R<VAR>p : R[X]<VAR>Semiring S<VAR>Nontrivial S<VAR>f : R →+* S<GOAL>Polynomial.map f p = 0 ↔ p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>DivisionRing R<VAR>p : R[X]<VAR>Semiring S<VAR>Nontrivial S<VAR>f : R →+* S<VAR>hp : p ≠ 0<GOAL>Polynomial.map f p ≠ 0