ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<VAR>hf : ¬f %ₘ minpoly A pb.gen = 0<VAR>this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim<VAR>i : ℕ<VAR>hi : i < pb.dim<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((f %ₘ minpoly A pb.gen).coeff i • pb.gen ^ i) = (f %ₘ minpoly A pb.gen).coeff i • y ^ i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<VAR>hf : ¬f %ₘ minpoly A pb.gen = 0<VAR>this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim<VAR>i : ℕ<VAR>hi : i < pb.dim<GOAL>(f %ₘ minpoly A pb.gen).coeff i • ((pb.basis.constr A) fun i => y ^ ↑i) (pb.gen ^ i) = (f %ₘ minpoly A pb.gen).coeff i • y ^ i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<VAR>h✝ : Nontrivial A<VAR>hf : ¬f %ₘ minpoly A pb.gen = 0<VAR>this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim<VAR>i : ℕ<VAR>hi : i < pb.dim<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) (pb.gen ^ i) = y ^ i
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.L₀X₂ToP ≫ S.φ₁ = 0
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PseudoMetricSpace β<VAR>inst✝¹ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : IsEmpty α<GOAL>dist f g = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<GOAL>Nonempty (α ↪o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<GOAL>Nonempty (α ↪o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<VAR>x y : β<VAR>hxy : x < y<GOAL>Nonempty (α ↪o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<VAR>x y : β<VAR>hxy : x < y<VAR>a : β<VAR>ha : x < a ∧ a < y<GOAL>Nonempty (α ↪o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<VAR>x y : β<VAR>hxy : x < y<VAR>a : β<VAR>ha : x < a ∧ a < y<VAR>this : Nonempty ↑(Set.Ioo x y)<VAR>our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))<GOAL>Nonempty (α ↪o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<VAR>x y : β<VAR>hxy : x < y<VAR>a : β<VAR>ha : x < a ∧ a < y<VAR>this : Nonempty ↑(Set.Ioo x y)<VAR>our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))<VAR>F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯<GOAL>Nonempty (α ↪o β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<VAR>x y : β<VAR>hxy : x < y<VAR>a : β<VAR>ha : x < a ∧ a < y<VAR>this : Nonempty ↑(Set.Ioo x y)<VAR>our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))<VAR>F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯<VAR>a₁ a₂ : α<GOAL>a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<VAR>x y : β<VAR>hxy : x < y<VAR>a : β<VAR>ha : x < a ∧ a < y<VAR>this : Nonempty ↑(Set.Ioo x y)<VAR>our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))<VAR>F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯<VAR>a₁ a₂ : α<VAR>f : PartialIso α ↑(Set.Ioo x y)<VAR>hf : f ∈ our_ideal<VAR>ha₁ : (a₁, ↑(F a₁)) ∈ ↑f<GOAL>a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<VAR>x y : β<VAR>hxy : x < y<VAR>a : β<VAR>ha : x < a ∧ a < y<VAR>this : Nonempty ↑(Set.Ioo x y)<VAR>our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))<VAR>F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯<VAR>a₁ a₂ : α<VAR>f : PartialIso α ↑(Set.Ioo x y)<VAR>hf : f ∈ our_ideal<VAR>ha₁ : (a₁, ↑(F a₁)) ∈ ↑f<VAR>g : PartialIso α ↑(Set.Ioo x y)<VAR>hg : g ∈ our_ideal<VAR>ha₂ : (a₂, ↑(F a₂)) ∈ ↑g<GOAL>a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : Countable α<VAR>inst✝¹ : DenselyOrdered β<VAR>inst✝ : Nontrivial β<VAR>val✝ : Encodable α<VAR>x y : β<VAR>hxy : x < y<VAR>a : β<VAR>ha : x < a ∧ a < y<VAR>this : Nonempty ↑(Set.Ioo x y)<VAR>our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))<VAR>F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯<VAR>a₁ a₂ : α<VAR>f : PartialIso α ↑(Set.Ioo x y)<VAR>hf : f ∈ our_ideal<VAR>ha₁ : (a₁, ↑(F a₁)) ∈ ↑f<VAR>g : PartialIso α ↑(Set.Ioo x y)<VAR>hg : g ∈ our_ideal<VAR>ha₂ : (a₂, ↑(F a₂)) ∈ ↑g<VAR>m : PartialIso α ↑(Set.Ioo x y)<VAR>_hm : m ∈ ↑our_ideal<VAR>fm : f ≤ m<VAR>gm : g ≤ m<GOAL>a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>root : (aeval pb.gen) p = 0<GOAL>pb.dim ≤ p.natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>root : (aeval pb.gen) p = 0<VAR>hlt : p.natDegree < pb.dim<GOAL>p = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>root : (aeval pb.gen) p = 0<VAR>hlt : p.natDegree < pb.dim<GOAL>∑ i : Fin pb.dim, (monomial ↑i) (p.coeff ↑i) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>root : (aeval pb.gen) p = 0<VAR>hlt : p.natDegree < pb.dim<VAR>i : Fin pb.dim<GOAL>(monomial ↑i) (p.coeff ↑i) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>hlt : p.natDegree < pb.dim<VAR>i : Fin pb.dim<VAR>root : ∑ x : Fin pb.dim, p.coeff ↑x • pb.basis x = 0<GOAL>(monomial ↑i) (p.coeff ↑i) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra A S<VAR>pb : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>hlt : p.natDegree < pb.dim<VAR>i : Fin pb.dim<VAR>root : ∑ x : Fin pb.dim, p.coeff ↑x • pb.basis x = 0<VAR>this : ∀ (i : Fin pb.dim), p.coeff ↑i = 0<GOAL>(monomial ↑i) (p.coeff ↑i) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>preNormEDS b c d 0 = 0
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>h_lub : IsLUB (Set.Iio i) i<VAR>hi_min : ¬IsMin i<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>h_lub : IsLUB (Set.Iio i) i<VAR>hi_min : ¬IsMin i<VAR>seq : ℕ → ι<VAR>h_tendsto : Tendsto seq atTop (𝓝 i)<VAR>h_bound : ∀ (j : ℕ), seq j < i<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>h_lub : IsLUB (Set.Iio i) i<VAR>hi_min : ¬IsMin i<VAR>seq : ℕ → ι<VAR>h_tendsto : Tendsto seq atTop (𝓝 i)<VAR>h_bound : ∀ (j : ℕ), seq j < i<VAR>h_Ioi_eq_Union : Set.Iio i = ⋃ j, {k | k ≤ seq j}<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>h_lub : IsLUB (Set.Iio i) i<VAR>hi_min : ¬IsMin i<VAR>seq : ℕ → ι<VAR>h_tendsto : Tendsto seq atTop (𝓝 i)<VAR>h_bound : ∀ (j : ℕ), seq j < i<VAR>h_Ioi_eq_Union : Set.Iio i = ⋃ j, {k | k ≤ seq j}<VAR>h_lt_eq_preimage : {ω | τ ω < i} = τ ⁻¹' Set.Iio i<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>h_lub : IsLUB (Set.Iio i) i<VAR>hi_min : ¬IsMin i<VAR>seq : ℕ → ι<VAR>h_tendsto : Tendsto seq atTop (𝓝 i)<VAR>h_bound : ∀ (j : ℕ), seq j < i<VAR>h_Ioi_eq_Union : Set.Iio i = ⋃ j, {k | k ≤ seq j}<VAR>h_lt_eq_preimage : {ω | τ ω < i} = τ ⁻¹' Set.Iio i<GOAL>MeasurableSet (τ ⁻¹' ⋃ j, {k | k ≤ seq j})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>h_lub : IsLUB (Set.Iio i) i<VAR>hi_min : ¬IsMin i<VAR>seq : ℕ → ι<VAR>h_tendsto : Tendsto seq atTop (𝓝 i)<VAR>h_bound : ∀ (j : ℕ), seq j < i<VAR>h_Ioi_eq_Union : Set.Iio i = ⋃ j, {k | k ≤ seq j}<VAR>h_lt_eq_preimage : {ω | τ ω < i} = τ ⁻¹' Set.Iio i<GOAL>MeasurableSet (⋃ i, {a | τ a ≤ seq i})
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>A A' : Matrix ι ι R<VAR>f f' : Module.End R M<VAR>h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f<VAR>h' : (PiToModule.fromMatrix R b) A' = (PiToModule.fromEnd R b) f'<GOAL>(PiToModule.fromMatrix R b) (A + A') = (PiToModule.fromEnd R b) (f + f')
<VAR>p : ℕ<VAR>hp : Nat.blt 1 p = true<VAR>h : sMod' (2 ^ p - 1) (p - 2) = 0<GOAL>LucasLehmerTest p
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>h : sMod' (2 ^ p - 1) (p - 2) = 0<GOAL>LucasLehmerTest p
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>h : sMod' (2 ^ p - 1) (p - 2) = 0<GOAL>↑0 = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v w : Fin 3 → R<GOAL>(crossProduct v) w + (crossProduct w) v = 0
<VAR>𝕜 : Type u<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>inst✝ : PartialOrder 𝕜<GOAL>HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Archimedean α<VAR>a : α<GOAL>⋃ n, Ico (↑n) (↑n + 1) = univ
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A X : C<VAR>inst✝ : IsConnected A<VAR>a : ↑(F.obj A)<VAR>f g : A ⟶ X<VAR>h : F.map f a = F.map g a<GOAL>f = g
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>A X : C<VAR>inst✝ : IsConnected A<VAR>a : ↑(F.obj A)<VAR>f g : A ⟶ X<VAR>h : F.map f a = F.map g a<VAR>this : IsIso (equalizer.ι f g)<GOAL>f = g
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h : a ≠ 0<VAR>s : Set ℝ<GOAL>(Measure.map (fun x => a * x) volume) s = ofReal |a⁻¹| * volume s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u s : Set α<GOAL>¬IsEmpty ↑s ↔ ¬s = ∅
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b✝ : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>b : B<GOAL>Multiset.count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b✝ : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>b : B<GOAL>(Multiset.map (fun a => X - C a) (Multiset.replicate (Multiset.count b (Multiset.map (⇑f) p.roots)) b)).prod ∣ map f p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b✝ : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>b : B<GOAL>(Multiset.map (fun a => X - C a) (Multiset.filter (Eq b) (Multiset.map (⇑f) p.roots))).prod ∣ map f p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b✝ : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>b : B<GOAL>(Multiset.map (fun a => X - C a) (Multiset.map (⇑f) p.roots)).prod ∣ map f p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b✝ : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>b : B<GOAL>(Multiset.map (fun a => X - C a) (Multiset.map (⇑f) p.roots)).prod = map f (Multiset.map (fun a => X - C a) p.roots).prod
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b✝ : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>b : B<GOAL>(Multiset.map ((fun a => X - C a) ∘ ⇑f) p.roots).prod = (Multiset.map (map f ∘ fun a => X - C a) p.roots).prod
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b✝ : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hmap : map f p ≠ 0<VAR>b : B<VAR>x✝ : A<GOAL>((fun a => X - C a) ∘ ⇑f) x✝ = (map f ∘ fun a => X - C a) x✝
<VAR>R S : Type u<VAR>M✝ : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : AddCommGroup M✝<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M✝<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : StrongRankCondition R<VAR>inst✝⁴ : Module.Free R M✝<VAR>inst✝³ : Module.Free R M'<VAR>ι : Type v<VAR>M : ι → Type w<VAR>inst✝² : (i : ι) → AddCommGroup (M i)<VAR>inst✝¹ : (i : ι) → Module R (M i)<VAR>inst✝ : ∀ (i : ι), Module.Free R (M i)<VAR>B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i => chooseBasis R (M i)<VAR>b : Basis ((i : ι) × ChooseBasisIndex R (M i)) R (⨁ (i : ι), M i) := DFinsupp.basis fun i => B i<GOAL>Module.rank R (⨁ (i : ι), M i) = sum fun i => Module.rank R (M i)
<VAR>u v : ℤ<VAR>n : ℕ<GOAL>IsUnit ↑n ↔ IsUnit n
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>√x ≤ √y ↔ x ≤ y
<VAR>x y : ℝ<VAR>hx : 0 < x<VAR>hy : y ≤ 0<GOAL>√x ≤ √y ↔ x ≤ y
<VAR>x y : ℝ<VAR>hx : 0 < x<VAR>hy : 0 ≤ y<GOAL>√x ≤ √y ↔ x ≤ y
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>f : ι →₀ R<VAR>i : ι<GOAL>((Finsupp.total ι (Dual R M) R ⇑b.dualBasis) f) (b i) = f i
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>f : ι →₀ R<VAR>i : ι<VAR>val✝ : Fintype ι<GOAL>((Finsupp.total ι (Dual R M) R ⇑b.dualBasis) f) (b i) = f i
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>f : ι →₀ R<VAR>i : ι<VAR>val✝ : Fintype ι<GOAL>∑ d : ι, (f d • b.dualBasis d) (b i) = f i
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>f : ι →₀ R<VAR>i : ι<VAR>val✝ : Fintype ι<GOAL>∀ (i : ι), 0 • b.dualBasis i = 0
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>hf : LSeriesSummable f s<VAR>hg : LSeriesSummable g s<GOAL>LSeriesSummable (f + g) s
<VAR>k : ℕ<VAR>hk : 2 ≤ k<GOAL>Summable fun n => -↑k ! / (2 * ↑π * I * ↑n) ^ k
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)<GOAL>Summable fun n => -↑k ! / (2 * ↑π * I * ↑n) ^ k
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)<GOAL>Summable fun n => -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)<GOAL>Summable fun a => ‖1 / ↑a ^ k‖
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)<VAR>this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|<GOAL>Summable fun a => ‖1 / ↑a ^ k‖
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)<VAR>this : (fun x => ‖1 / ↑x ^ k‖) = fun x => |1 / ↑x ^ k|<GOAL>Summable fun x => |1 / ↑x ^ k|
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hs : s ≠ ∅<GOAL>(indiscrete hs).IsEquipartition
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hs : s ≠ ∅<GOAL>{s}.EquitableOn Finset.card
<VAR>α : Type u_1<VAR>inst✝³ : Zero α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : a ≠ 0<GOAL>ContinuousAt (⇑SignType.sign) a
<VAR>α : Type u_1<VAR>inst✝³ : Zero α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : a ≠ 0<VAR>h_neg : a < 0<GOAL>ContinuousAt (⇑SignType.sign) a
<VAR>α : Type u_1<VAR>inst✝³ : Zero α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : a ≠ 0<VAR>h_pos : 0 < a<GOAL>ContinuousAt (⇑SignType.sign) a
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<GOAL>1 * 1 + 0 * x = 1
<VAR>a b c : ℕ<VAR>h : a ≤ b<GOAL>Ico a (b + 1) = insert b (Ico a b)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a✝)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>ι : Type u_3<VAR>f : ι → R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (∀ (i : ι), ContinuousOn (f i) (σₙ R a)) _auto✝<VAR>hf0 : autoParam (∀ (i : ι), f i 0 = 0) _auto✝<VAR>i : ι<GOAL>cfcₙ (f i) a = (cfcₙHom ha) { toFun := (σₙ R a).restrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f < g<VAR>gh : g < h<GOAL>(h - f).Pos
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f < g<VAR>gh : g < h<GOAL>h - f = g - f + (h - g)
<VAR>m n : ℤ<GOAL>¬Odd n ↔ n % 2 = 0