ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A / C⁻¹).card * B.card ≤ (A / B).card * (B / C⁻¹).card
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>M N : Matrix n n A<GOAL>invFun R A n (M + N) = invFun R A n M + invFun R A n N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<VAR>x : α<VAR>h : x ∉ t<GOAL>insert x s \ t = insert x (s \ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<VAR>x : α<VAR>h : x ∉ t<GOAL>insert x ↑s \ ↑t = insert x (↑s \ ↑t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t : Set α<VAR>i : ι✝<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>ι : Type u_6<VAR>s : ι → Set α<GOAL>(⨅ i, 𝓟 (s i)).HasBasis (fun t => t.Finite) fun t => ⋂ i ∈ t, s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t : Set α<VAR>i : ι✝<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>ι : Type u_6<VAR>s : ι → Set α<VAR>U : Set α<GOAL>(∃ t, U ∈ ⨅ i ∈ t, 𝓟 (s i)) ↔ ∃ i, i.Finite ∧ ⋂ i_1 ∈ i, s i_1 ⊆ U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>Set.range ⇑(pullback.fst g f).val.base = ((Opens.map g.val.base).obj { carrier := Set.range ⇑f.val.base, is_open' := ⋯ }).carrier
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>⇑(pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f)) '' (⇑(pullback.snd g.val.base f.val.base) ⁻¹' Set.univ) = ((Opens.map g.val.base).obj { carrier := Set.range ⇑f.val.base, is_open' := ⋯ }).carrier
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>Function.Surjective ⇑(PreservesPullback.iso Scheme.forgetToTop g f).hom
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>Epi (PreservesPullback.iso Scheme.forgetToTop g f).hom
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<VAR>hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0<GOAL>Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom = Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom + Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<VAR>hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0<GOAL>Polynomial.eval₂ f a (x + y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) = (Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.denom + Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.num) * Polynomial.eval₂ f a (x + y).denom
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<VAR>hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0<GOAL>Polynomial.eval₂ f a ((x + y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a ((x.num * y.denom + x.denom * y.num) * (x + y).denom)
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x y : RatFunc K<VAR>hx : Polynomial.eval₂ f a x.denom ≠ 0<VAR>hy : Polynomial.eval₂ f a y.denom ≠ 0<VAR>hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0<GOAL>(x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<GOAL>∃ x, c < ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<VAR>x : E<VAR>hx : x ≠ 0<GOAL>∃ x, c < ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<VAR>x : E<VAR>hx : x ≠ 0<VAR>r : 𝕜<VAR>hr : c / ‖x‖ < ‖r‖<GOAL>∃ x, c < ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<VAR>x : E<VAR>hx : x ≠ 0<VAR>r : 𝕜<VAR>hr : c / ‖x‖ < ‖r‖<GOAL>c < ‖r • x‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : Nontrivial E<VAR>c : ℝ<VAR>x : E<VAR>hx : x ≠ 0<VAR>r : 𝕜<VAR>hr : c / ‖x‖ < ‖r‖<GOAL>0 < ‖x‖
<VAR>m n : ℕ∞<GOAL>↑(m + n) = ↑m + ↑n
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<GOAL>(cyclotomic n K).IsRoot μ ↔ IsPrimitiveRoot μ n
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<GOAL>(cyclotomic n K).IsRoot μ ↔ IsPrimitiveRoot μ n
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<GOAL>IsPrimitiveRoot μ n
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : μ ^ n = 1<GOAL>IsPrimitiveRoot μ n
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : μ ^ n = 1<VAR>hnμ : ¬IsPrimitiveRoot μ n<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : μ ^ n = 1<VAR>hnμ : ¬IsPrimitiveRoot μ n<VAR>ho : 0 < orderOf μ<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : μ ^ n = 1<VAR>hnμ : ¬IsPrimitiveRoot μ n<VAR>ho : 0 < orderOf μ<VAR>this : μ ^ orderOf μ = 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : μ ^ n = 1<VAR>hnμ : ¬IsPrimitiveRoot μ n<VAR>ho : 0 < orderOf μ<VAR>this : ∃ i ∈ (orderOf μ).divisors, (cyclotomic i K).IsRoot μ<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : μ ^ n = 1<VAR>hnμ : ¬IsPrimitiveRoot μ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hio : i ∈ (orderOf μ).divisors<VAR>hiμ : (cyclotomic i K).IsRoot μ<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : μ ^ n = 1<VAR>hnμ : ¬IsPrimitiveRoot μ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hiμ : (cyclotomic i K).IsRoot μ<VAR>hio : i ∣ orderOf μ<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : μ ^ n = 1<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hiμ : (cyclotomic i K).IsRoot μ<VAR>hio : i ∣ orderOf μ<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hiμ : (cyclotomic i K).IsRoot μ<VAR>hio : i ∣ orderOf μ<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hiμ : (cyclotomic i K).IsRoot μ<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : (cyclotomic n K).IsRoot μ<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hiμ : (cyclotomic i K).IsRoot μ<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<VAR>key' : i ∣ n<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : X - C μ ∣ cyclotomic n K<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hiμ : X - C μ ∣ cyclotomic i K<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<VAR>key' : i ∣ n<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμ : X - C μ ∣ cyclotomic n K<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hiμ : X - C μ ∣ cyclotomic i K<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<VAR>key' : i ∣ n<VAR>hni : {i, n} ⊆ n.divisors<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<VAR>key' : i ∣ n<VAR>hni : {i, n} ⊆ n.divisors<VAR>k : K[X]<VAR>hk : cyclotomic i K = (X - C μ) * k<VAR>j : K[X]<VAR>hj : cyclotomic n K = (X - C μ) * j<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<VAR>key' : i ∣ n<VAR>hni : {i, n} ⊆ n.divisors<VAR>k : K[X]<VAR>hk : cyclotomic i K = (X - C μ) * k<VAR>j : K[X]<VAR>hj : cyclotomic n K = (X - C μ) * j<VAR>this : ∏ i ∈ n.divisors, cyclotomic i K = X ^ n - 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<VAR>key' : i ∣ n<VAR>hni : {i, n} ⊆ n.divisors<VAR>k : K[X]<VAR>hk : cyclotomic i K = (X - C μ) * k<VAR>j : K[X]<VAR>hj : cyclotomic n K = (X - C μ) * j<VAR>this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<VAR>key' : i ∣ n<VAR>hni : {i, n} ⊆ n.divisors<VAR>k : K[X]<VAR>hk : cyclotomic i K = (X - C μ) * k<VAR>j : K[X]<VAR>hj : cyclotomic n K = (X - C μ) * j<VAR>this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1<VAR>hn : Squarefree (X ^ n - 1)<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>n✝ : ℕ<VAR>inst✝² : IsDomain R<VAR>n : ℕ<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>μ : K<VAR>inst✝ : NeZero ↑n<VAR>hnpos : 0 < n<VAR>hμn : orderOf μ ∣ n<VAR>hnμ : orderOf μ ≠ n<VAR>ho : 0 < orderOf μ<VAR>i : ℕ<VAR>hio : i ∣ orderOf μ<VAR>key : i < n<VAR>key' : i ∣ n<VAR>hni : {i, n} ⊆ n.divisors<VAR>k : K[X]<VAR>hk : cyclotomic i K = (X - C μ) * k<VAR>j : K[X]<VAR>hj : cyclotomic n K = (X - C μ) * j<VAR>this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1<VAR>hn : IsUnit (X - C μ)<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>Flat R M ↔ Baer R (CharacterModule M)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type w<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>(∀ (I : Ideal R) (b : ↥I →ₗ[R] CharacterModule M), ∃ a, ∀ (a_1 : R) (b_1 : a_1 ∈ I) (x : M), (((lcomp R (CharacterModule M) (Submodule.subtype I)) a) ⟨a_1, b_1⟩) x = (b ⟨a_1, b_1⟩) x) ↔ ∀ (I : Ideal R) (g : ↥I →ₗ[R] CharacterModule M), ∃ g', ∀ (x : R) (mem : x ∈ I) (x_1 : M), (g' x) x_1 = (g ⟨x, mem⟩) x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>hx : ∀ b ∈ s, a < b<GOAL>(insert a s).chainHeight = s.chainHeight + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>hx : ∀ b ∈ s, a < b<GOAL>(insert a s).chainHeight + 0 = s.chainHeight + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>hx : ∀ b ∈ s, a < b<GOAL>(insert a s).chainHeight + ↑0 = s.chainHeight + ↑1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>hx : ∀ b ∈ s, a < b<GOAL>∀ l ∈ (insert a s).subchain, ∃ l' ∈ s.subchain, l.length + 0 ≤ l'.length + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>hx : ∀ b ∈ s, a < b<GOAL>∀ l ∈ s.subchain, ∃ l' ∈ (insert a s).subchain, l.length + 1 ≤ l'.length + 0
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>x : Γ₀<VAR>h : x ≠ 0<GOAL>(𝓝 x).HasBasis (fun x => True) fun x_1 => {x}
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>x : Γ₀<VAR>h : x ≠ 0<GOAL>(pure x).HasBasis (fun x => True) fun x_1 => {x}
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<GOAL>l.revzip.length = l.length
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a n x✝ : M<GOAL>x✝ ∈ powers n ↔ x✝ ∈ closure {n}
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>ω.length = ω.length ∧ cs.wordProd ω = cs.wordProd ω
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : LocallyFiniteOrderTop α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a a✝ : α<GOAL>a✝ ∈ (Ioi a).disjUnion (Iio a) ⋯ ↔ a✝ ∈ {a}ᶜ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>hp : 0 < p.natDegree<GOAL>(derivative p).degree = ↑(p.natDegree - 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>hp : 0 < p.natDegree<GOAL>(derivative p).degree ≤ ↑(p.natDegree - 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>hp : 0 < p.natDegree<GOAL>↑(p.natDegree - 1) ≤ (derivative p).degree
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<VAR>this : CompleteSpace E<GOAL>⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<VAR>this✝ : CompleteSpace E<VAR>this : CompleteSpace F<GOAL>⟪x, (adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>x : E<VAR>y : F<VAR>this✝ : CompleteSpace E<VAR>this : CompleteSpace F<GOAL>⟪x, ↑(ContinuousLinearMap.adjoint (toContinuousLinearMap ↑(toContinuousLinearMap A))) y⟫_𝕜 = ⟪↑(toContinuousLinearMap A) x, y⟫_𝕜
<VAR>n a : ℕ<VAR>l : List ℕ<VAR>hl : (a :: l).IsZeckendorfRep<VAR>hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n<GOAL>(map fib (a :: l)).sum < fib n
<VAR>n a : ℕ<VAR>l : List ℕ<VAR>hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n<VAR>hl : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun a b => b + 2 ≤ a) (l ++ [0])<GOAL>(map fib (a :: l)).sum < fib n
<VAR>n a : ℕ<VAR>l : List ℕ<VAR>hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n<VAR>hl : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun a b => b + 2 ≤ a) (l ++ [0])<VAR>this : ∀ b ∈ (l ++ [0]).head?, b < a - 1<GOAL>(map fib (a :: l)).sum < fib n
<VAR>n a : ℕ<VAR>l : List ℕ<VAR>hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n<VAR>this : ∀ b ∈ (l ++ [0]).head?, b < a - 1<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<GOAL>(map fib (a :: l)).sum < fib n
<VAR>n a : ℕ<VAR>l : List ℕ<VAR>hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n<VAR>this : ∀ b ∈ (l ++ [0]).head?, b < a - 1<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<GOAL>fib a + (map fib l).sum < fib n
<VAR>n a : ℕ<VAR>l : List ℕ<VAR>hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n<VAR>this : ∀ b ∈ (l ++ [0]).head?, b < a - 1<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<GOAL>fib a + fib (a - 1) ≤ fib n
<VAR>n a : ℕ<VAR>l : List ℕ<VAR>hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n<VAR>this : ∀ b ∈ (l ++ [0]).head?, b < a - 1<VAR>hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ Chain' (fun a b => b + 2 ≤ a) (l ++ [0])<GOAL>fib (a + 1) ≤ fib n
<VAR>m n k : ℕ<GOAL>(k * n + m).Coprime n ↔ m.Coprime n
<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>n : Type w<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>i j : n<VAR>x : A<VAR>t : ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)<GOAL>(matrixEquivTensor R A n) (stdBasisMatrix i j x) = x ⊗ₜ[R] stdBasisMatrix i j 1
<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>x✝ : AddCircle p<VAR>ε : ℝ<VAR>hε : |p| / 2 ≤ ε<VAR>x : AddCircle p<GOAL>x ∈ closedBall x✝ ε
<VAR>θ : ℝ<VAR>h0 : 0 ≤ θ<VAR>hpi : θ ≤ π<GOAL>(-↑θ).sign ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : MeasurableSpace β<VAR>ν : Measure β<VAR>f : α → β<VAR>g : β →ₘ[ν] γ<VAR>hf : QuasiMeasurePreserving f μ ν<GOAL>g.compQuasiMeasurePreserving f hf = mk (↑g ∘ f) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o o' : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>g : (a : Ordinal.{u}) → a < o' → Ordinal.{max u v}<VAR>h : o.brange f ⊆ o'.brange g<GOAL>range (o.familyOfBFamily f) ⊆ range (o'.familyOfBFamily g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝¹ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I✝ : Set α<VAR>M : Matroid α<VAR>I : Set ↑X<GOAL>(M.restrictSubtype X).Indep I ↔ M.Indep ↑I
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>χ : DirichletCharacter R 1<GOAL>χ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>j i : ι<VAR>hij : i ≤ j<GOAL>gramSchmidt 𝕜 f i ∈ span 𝕜 (f '' Set.Iic j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>j i : ι<VAR>hij : i ≤ j<GOAL>f i - ∑ i_1 ∈ Finset.Iio i, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i_1})) (f i)) ∈ span 𝕜 (f '' Set.Iic j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>j i : ι<VAR>hij : i ≤ j<GOAL>f i - ∑ x ∈ Finset.Iio i, (⟪gramSchmidt 𝕜 f x, f i⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f x‖ ^ 2)) • gramSchmidt 𝕜 f x ∈ span 𝕜 (f '' Set.Iic j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>j i : ι<VAR>hij : i ≤ j<VAR>k : ι<VAR>hk : k ∈ Finset.Iio i<GOAL>(⟪gramSchmidt 𝕜 f k, f i⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f k‖ ^ 2)) • gramSchmidt 𝕜 f k ∈ span 𝕜 (f '' Set.Iic j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>j i : ι<VAR>hij : i ≤ j<VAR>k : ι<VAR>hk : k ∈ Finset.Iio i<VAR>hkj : k < j := LT.lt.trans_le (Finset.mem_Iio.mp hk) hij<GOAL>(⟪gramSchmidt 𝕜 f k, f i⟫_𝕜 / ↑(‖gramSchmidt 𝕜 f k‖ ^ 2)) • gramSchmidt 𝕜 f k ∈ span 𝕜 (f '' Set.Iic j)
<VAR>a✝ b✝ m n p✝ a b p : ℕ<GOAL>a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)