ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜₁ : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝¹⁸ : NormedAddCommGroup F₁<VAR>inst✝¹⁷ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup F₂<VAR>inst✝¹² : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁸ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁶ : FiberBundle F₁ E₁<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁴ : FiberBundle F₂ E₂<VAR>inst✝³ : Trivialization.IsLinear 𝕜₁ e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜₁ e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜₂ e₂'<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)<VAR>L : F₁ →SL[σ] F₂<VAR>v : F₁<GOAL>((continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b) L) v = (↑(continuousLinearMap σ e₁' e₂') { proj := b, snd := (continuousLinearMap σ e₁ e₂).symm b L }).2 v
<VAR>𝕜₁ : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝¹⁸ : NormedAddCommGroup F₁<VAR>inst✝¹⁷ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup F₂<VAR>inst✝¹² : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁸ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁶ : FiberBundle F₁ E₁<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁴ : FiberBundle F₂ E₂<VAR>inst✝³ : Trivialization.IsLinear 𝕜₁ e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜₁ e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜₂ e₂'<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)<VAR>L : F₁ →SL[σ] F₂<VAR>v : F₁<GOAL>(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b) (L ((Trivialization.coordChangeL 𝕜₁ e₁' e₁ b) v)) = (Trivialization.linearMapAt 𝕜₂ e₂' b) (e₂.symm b (L ((Trivialization.linearMapAt 𝕜₁ e₁ b) (e₁'.symm b v))))
<VAR>𝕜₁ : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝¹⁸ : NormedAddCommGroup F₁<VAR>inst✝¹⁷ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup F₂<VAR>inst✝¹² : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁸ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁶ : FiberBundle F₁ E₁<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁴ : FiberBundle F₂ E₂<VAR>inst✝³ : Trivialization.IsLinear 𝕜₁ e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜₁ e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜₂ e₂'<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)<VAR>L : F₁ →SL[σ] F₂<VAR>v : F₁<GOAL>b ∈ e₁'.baseSet ∩ e₁.baseSet
<VAR>𝕜₁ : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝¹⁸ : NormedAddCommGroup F₁<VAR>inst✝¹⁷ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup F₂<VAR>inst✝¹² : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁸ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁶ : FiberBundle F₁ E₁<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁴ : FiberBundle F₂ E₂<VAR>inst✝³ : Trivialization.IsLinear 𝕜₁ e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜₁ e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜₂ e₂'<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)<VAR>L : F₁ →SL[σ] F₂<VAR>v : F₁<GOAL>b ∈ e₂.baseSet ∩ e₂'.baseSet
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : a < b<VAR>hc : 0 < c<GOAL>a / c < b / c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : a < b<VAR>hc : 0 < c<GOAL>a * (1 / c) < b * (1 / c)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝ : EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<GOAL>𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<GOAL>(M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑(Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<GOAL>(∑ x ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign x) * ∏ i : n, M.charmatrix (x i) i + ↑↑(Equiv.Perm.sign (Equiv.refl n)) * ∏ i : n, M.charmatrix ((Equiv.refl n) i) i - ∏ i : n, (X - C (M i i))).degree < ↑(Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<GOAL>(∑ x ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign x) * ∏ i : n, M.charmatrix (x i) i).degree < ↑(Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<GOAL>∑ x ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign x) * ∏ i : n, M.charmatrix (x i) i ∈ degreeLT R (Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<GOAL>∀ c ∈ univ.erase (Equiv.refl n), ↑↑(Equiv.Perm.sign c) * ∏ i : n, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>↑↑(Equiv.Perm.sign c) * ∏ i : n, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>↑↑(Equiv.Perm.sign c) • ∏ i : n, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>∏ i : n, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>(∏ i : n, M.charmatrix (c i) i).degree < ↑(Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>↑(∏ i : n, M.charmatrix (c i) i).natDegree < ↑(Fintype.card n - 1)
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>(∏ i : n, M.charmatrix (c i) i).natDegree < Fintype.card n - 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>(∏ i : n, M.charmatrix (c i) i).natDegree ≤ (filter (fun x => c x = x) univ).card
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>∑ i : n, (M.charmatrix (c i) i).natDegree ≤ (filter (fun x => c x = x) univ).card
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>∑ i : n, (M.charmatrix (c i) i).natDegree ≤ ∑ x ∈ filter (fun x => c x = x) univ, 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>∑ i : n, (M.charmatrix (c i) i).natDegree ≤ ∑ a : n, if c a = a then 1 else 0
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<GOAL>∀ i ∈ univ, (M.charmatrix (c i) i).natDegree ≤ if c i = i then 1 else 0
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M : Matrix n n R<VAR>c : n ≃ n<VAR>hc : c ∈ univ.erase (Equiv.refl n)<VAR>i✝ : n<VAR>a✝ : i✝ ∈ univ<GOAL>(M.charmatrix (c i✝) i✝).natDegree ≤ if c i✝ = i✝ then 1 else 0
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>f : M ≃[L] N<VAR>n : N<GOAL>n ∈ f.toHom.range ↔ n ∈ ⊤
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>f : M ≃[L] N<VAR>n : N<GOAL>∃ y, f y = n
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Finite m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>inst✝¹ : Fintype l<VAR>inst✝ : DecidableEq l<VAR>b : Basis l R M₁<VAR>b' : Basis l R M₂<VAR>i j : l<GOAL>(toMatrix b' b) (↑(b'.equiv b (Equiv.refl l))) i j = 1 i j
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : CommRing L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>hn : n ≠ 2<VAR>hirr : Irreducible (cyclotomic (↑n) K)<GOAL>(Algebra.norm K) ζ = 1
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : CommRing L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>hn : n ≠ 2<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this : NeZero ↑↑n<GOAL>(Algebra.norm K) ζ = 1
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<GOAL>((expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).sin * ‖x + y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (x + y)).sin * ‖x + y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (y + x)).sin * ‖y + x‖ = ‖x‖
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>z : N<GOAL>(f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>T' : Type u_8<VAR>inst✝⁴ : NonAssocSemiring R<VAR>inst✝³ : NonAssocSemiring S<VAR>inst✝² : NonAssocSemiring R'<VAR>inst✝¹ : NonAssocSemiring S'<VAR>inst✝ : Subsingleton S<VAR>fst✝ : S<VAR>snd✝ : R<GOAL>(fun x => (0, x)) (fst✝, snd✝).2 = (fst✝, snd✝)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>a : ℝ<GOAL>LipschitzWith Kf fun x => max a (f x)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>kernel.ι f ≫ factorThruImage f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>coequalizer.π (kernel.ι f) 0 ≫ (coimageIsoImage' f).hom = coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) (factorThruImage f) ⋯
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>f : V₁ →ₗ[K] V₂<GOAL>Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => min (f b) (g b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => if f b ≤ g b then f b else g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : SingleObj α ⥤q SingleObj β<VAR>g : SingleObj β ⥤q SingleObj γ<GOAL>toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra ℝ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ht : spectralRadius ℝ a ≤ ↑t<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra ℝ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ht : spectralRadius ℝ a ≤ ↑t<VAR>this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t<GOAL>SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra ℝ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ht : spectralRadius ℝ a ≤ ↑t<VAR>this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t<GOAL>(∀ x ∈ spectrum ℝ a, 0 ≤ x) ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra ℝ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ht : spectralRadius ℝ a ≤ ↑t<VAR>this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t<VAR>h : ∀ x ∈ spectrum ℝ a, 0 ≤ x<VAR>x : ℝ<VAR>hx : x ∈ spectrum ℝ ((algebraMap ℝ A) ↑t - a)<GOAL>↑‖x‖₊ ≤ ↑t
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra ℝ A<VAR>a : A<VAR>t : ℝ≥0<VAR>ht : spectralRadius ℝ a ≤ ↑t<VAR>this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t<VAR>h : spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t<GOAL>∀ x ∈ spectrum ℝ a, 0 ≤ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<GOAL>a + b ∈ carrier f_deg q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<GOAL>HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<GOAL>HomogeneousLocalization.mk { deg := { deg := m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.deg + { deg := m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.deg, num := ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num * ↑{ deg := m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num, ⋯⟩, den := ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den * ↑{ deg := m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<GOAL>HomogeneousLocalization.mk { deg := m * i + m * i, num := ⟨(proj 𝒜 i) (a + b) ^ m * (proj 𝒜 i) (a + b) ^ m, ⋯⟩, den := ⟨f ^ i * f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<GOAL>HomogeneousLocalization.mk { deg := m * i + m * i, num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩, den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<GOAL>HomogeneousLocalization.mk { deg := m * i + m * i, num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩, den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i j : ℕ<VAR>h2 : ¬m + m < j<VAR>h1 : j ≤ m<GOAL>(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j) ∈ 𝒜 (m * i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i j : ℕ<VAR>h2 : ¬m + m < j<VAR>h1 : ¬j ≤ m<VAR>l : A⁰_ f := HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<GOAL>(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j) ∈ 𝒜 (m * i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<GOAL>HomogeneousLocalization.mk { deg := m * i + m * i, num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩, den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ } = ∑ i ∈ range (m + m + 1), g i