ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hG : IsPGroup p G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>ϕ : H →* G<VAR>hϕ : Function.Injective ⇑ϕ<GOAL>∀ (g : H), ∃ k, ϕ g ^ p ^ k = 1
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoDiv hp (a + m • p) b = toIcoDiv hp a b - m
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>b - (toIcoDiv hp a b - m) • p ∈ Set.Ico (a + m • p) (a + m • p + p)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>b - toIcoDiv hp a b • p + m • p ∈ Set.Ico (a + m • p) (a + p + m • p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : LE α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a * b ≤ a<GOAL>a * b ≤ a * 1
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<VAR>hi : i ∈ s<GOAL>nodalWeight s v i = (eval (v i) (derivative (nodal s v)))⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>p✝ q✝ : R[X]<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>x : S<VAR>hx : eval₂ f x q = 0<GOAL>eval₂ f x (p %ₘ q) = eval₂ f x p
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>inst✝ : IsTrans α R<VAR>hl : Chain' R l₂<VAR>h : l₁ <+ l₂<GOAL>Chain' R l₁
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>inst✝ : IsTrans α R<VAR>hl : Pairwise R l₂<VAR>h : l₁ <+ l₂<GOAL>Pairwise R l₁
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : ¬Prime p<GOAL>n.factorization p = 0
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>h : ↥H<VAR>g : G<GOAL>hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>h : ↥H<VAR>g : G<VAR>this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2<GOAL>hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>h : ↥H<VAR>g : G<GOAL>RightCosetEquivalence (↑H) (↑h * g) g
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : Nonempty ((i : ι) → α i)<VAR>s t : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ t }) → α ↑i)<VAR>inst✝ : DecidableEq ι<GOAL>Disjoint (cylinder s S) (cylinder t T) ↔ Disjoint ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S) ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' T)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.1042846<VAR>S' : Type ?u.1042849<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.1045280<VAR>S'' : Type ?u.1045283<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>x : P.Cotangent<GOAL>((map (Hom.id P)) x).val = (LinearMap.id x).val
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.1042846<VAR>S' : Type ?u.1042849<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.1045280<VAR>S'' : Type ?u.1045283<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>x : ↥P.ker<GOAL>((map (Hom.id P)) (mk x)).val = (LinearMap.id (mk x)).val
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : Function.Surjective ⇑f<GOAL>↑(map f I) = Submodule.map ↑f ↑I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J✝ : LieIdeal R L'<VAR>h : Function.Surjective ⇑f<VAR>J : LieIdeal R L' := let __src := Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule; { toSubmodule := __src, lie_mem := ⋯ }<GOAL>↑(map f I) = Submodule.map ↑f ↑I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J✝ : LieIdeal R L'<VAR>h : Function.Surjective ⇑f<VAR>J : LieIdeal R L' := let __src := Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule; { toSubmodule := __src, lie_mem := ⋯ }<GOAL>∃ N, ↑N = Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule
<VAR>𝕜 : Type u_1<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>W₂ : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>Q₂ : Type u_8<VAR>inst✝¹⁶ : NormedAddCommGroup V<VAR>inst✝¹⁵ : MetricSpace P<VAR>inst✝¹⁴ : NormedAddTorsor V P<VAR>inst✝¹³ : NormedAddCommGroup W<VAR>inst✝¹² : MetricSpace Q<VAR>inst✝¹¹ : NormedAddTorsor W Q<VAR>inst✝¹⁰ : NormedAddCommGroup W₂<VAR>inst✝⁹ : MetricSpace Q₂<VAR>inst✝⁸ : NormedAddTorsor W₂ Q₂<VAR>inst✝⁷ : NormedField R<VAR>inst✝⁶ : NormedSpace R V<VAR>inst✝⁵ : NormedSpace R W<VAR>inst✝⁴ : NormedSpace R W₂<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 V<VAR>inst✝¹ : NormedSpace 𝕜 W<VAR>inst✝ : NormedSpace 𝕜 W₂<VAR>f : V →ᵃ[R] W<VAR>h : Continuous f.toFun<GOAL>⇑{ toAffineMap := f, cont := h } = ⇑{ toAffineMap := f, cont := h }.contLinear + Function.const V ({ toAffineMap := f, cont := h } 0)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s t✝ s₁✝ s₂✝ t₁ t₂ u : Set E<VAR>x y : E<VAR>s₁ s₂ t : Set E<GOAL>convexJoin 𝕜 (s₁ ∪ s₂) t = convexJoin 𝕜 s₁ t ∪ convexJoin 𝕜 s₂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>x : α →₀ M<GOAL>mapRange (⇑f.symm) hf' (mapRange (⇑f) hf x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>x : α →₀ M<GOAL>mapRange id ⋯ x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>x : α →₀ M<GOAL>id 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>x : α →₀ N<GOAL>mapRange (⇑f) hf (mapRange (⇑f.symm) hf' x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>x : α →₀ N<GOAL>mapRange id ⋯ x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M ≃ N<VAR>hf : f 0 = 0<VAR>hf' : f.symm 0 = 0<VAR>x : α →₀ N<GOAL>id 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>f : α → β<VAR>hi : Injective f<GOAL>(range f).Infinite ↔ Infinite α
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>a : R<VAR>b : B<VAR>m d : ℤ<GOAL>selfZPow x B (m - d) * mk' B a 1 = b ↔ selfZPow x B m * mk' B a 1 = selfZPow x B d * b
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>a : R<VAR>b : B<VAR>m d : ℤ<GOAL>selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b ↔ selfZPow x B m * mk' B a 1 = selfZPow x B d * b
<VAR>α : Type u_1<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (fun x => x + c) (Ioc a b) = Ioc (a + c) (b + c)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M N : PresheafOfModules R<VAR>f : M ⟶ N<VAR>s : M.sections<VAR>X Y : Cᵒᵖ<VAR>g : X ⟶ Y<GOAL>(N.map g) ((fun X => (Hom.app f X) (↑s X)) X) = (fun X => (Hom.app f X) (↑s X)) Y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>LinearMap.range (M.mulMap N) = M * N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<GOAL>LinearMap.range (M.mulMap N) ≤ M * N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>x : ↥M ⊗[R] ↥N<GOAL>(M.mulMap N) x ∈ M * N
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid A<VAR>s t u : Set M<VAR>H K : Submonoid M<GOAL>closure ↑H ⊔ closure ↑K ≤ H ⊔ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>f : α ↪ β<VAR>hG : G.EdgeDisjointTriangles<GOAL>(SimpleGraph.map f G).EdgeDisjointTriangles
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>f : α ↪ β<VAR>hG : G.EdgeDisjointTriangles<GOAL>(G.cliqueSet 3).Pairwise ((fun x y => (↑x ∩ ↑y).Subsingleton) on Finset.map f)
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : AddMonoid R<GOAL>closure IsSquare = SumSqIn R
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : AddMonoid R<VAR>x : R<VAR>hx : x ∈ SumSqIn R<GOAL>x ∈ closure IsSquare
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>inst✝ : DecidableEq ι<VAR>s : Set (α i)<VAR>x : (x : ι) → α x<GOAL>x ∈ eval i ⁻¹' s ↔ x ∈ univ.pi (update (fun i => univ) i s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>b : Basis ι R S<VAR>inst✝³ : Module.Free R S<VAR>inst✝² : Module.Free R T<VAR>inst✝¹ : Module.Finite R S<VAR>inst✝ : Module.Finite R T<VAR>x : S × T<VAR>a✝ : Nontrivial R<VAR>f : S × T →ₗ[R] Module.End R S × Module.End R T := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap<GOAL>(trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>b : Basis ι R S<VAR>inst✝³ : Module.Free R S<VAR>inst✝² : Module.Free R T<VAR>inst✝¹ : Module.Finite R S<VAR>inst✝ : Module.Finite R T<VAR>x : S × T<VAR>a✝ : Nontrivial R<VAR>f : S × T →ₗ[R] Module.End R S × Module.End R T := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap<VAR>this : (lmul R (S × T)).toLinearMap = prodMapLinear R S T S T R ∘ₗ f<GOAL>(trace R (S × T)) x = (trace R S) x.1 + (trace R T) x.2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : CommRing T<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra R T<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>b : Basis ι R S<VAR>inst✝³ : Module.Free R S<VAR>inst✝² : Module.Free R T<VAR>inst✝¹ : Module.Finite R S<VAR>inst✝ : Module.Finite R T<VAR>x : S × T<VAR>a✝ : Nontrivial R<VAR>f : S × T →ₗ[R] Module.End R S × Module.End R T := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap<VAR>this : (lmul R (S × T)).toLinearMap = prodMapLinear R S T S T R ∘ₗ f<GOAL>(LinearMap.trace R (S × T) ∘ₗ prodMapLinear R S T S T R ∘ₗ f) x = (LinearMap.trace R S ∘ₗ (lmul R S).toLinearMap) x.1 + (LinearMap.trace R T ∘ₗ (lmul R T).toLinearMap) x.2
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>(M ↾ X).Base I ↔ M.Basis I X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>(M.Indep I ∧ I ⊆ X ∧ ∀ (I_1 : Set α), M.Indep I_1 ∧ I_1 ⊆ X → I ⊆ I_1 → I = I_1) ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝⁴ : f.NeBot<VAR>R : Type u_7<VAR>inst✝³ : Preorder R<VAR>inst✝² : Add R<VAR>inst✝¹ : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u v : α → R<VAR>U : R<VAR>hU : ∀ᶠ (x : R) in map u f, (fun x x_1 => x ≤ x_1) x U<VAR>V : R<VAR>hV : ∀ᶠ (x : R) in map v f, (fun x x_1 => x ≤ x_1) x V<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) f (u + v)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝⁴ : f.NeBot<VAR>R : Type u_7<VAR>inst✝³ : Preorder R<VAR>inst✝² : Add R<VAR>inst✝¹ : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u v : α → R<VAR>U : R<VAR>hU : ∀ᶠ (x : R) in map u f, (fun x x_1 => x ≤ x_1) x U<VAR>V : R<VAR>hV : ∀ᶠ (x : R) in map v f, (fun x x_1 => x ≤ x_1) x V<GOAL>∀ᶠ (x : R) in map (u + v) f, (fun x x_1 => x ≤ x_1) x (U + V)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>f : Filter α<VAR>inst✝⁴ : f.NeBot<VAR>R : Type u_7<VAR>inst✝³ : Preorder R<VAR>inst✝² : Add R<VAR>inst✝¹ : CovariantClass R R (fun a b => a + b) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass R R (fun a b => b + a) fun x x_1 => x ≤ x_1<VAR>u v : α → R<VAR>U V : R<VAR>hU : ∀ᶠ (a : α) in f, u a ≤ U<VAR>hV : ∀ᶠ (a : α) in f, v a ≤ V<GOAL>∀ᶠ (a : α) in f, u a + v a ≤ U + V
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ ∪ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X : OppositeShift C A<VAR>a b : A<GOAL>(shiftFunctorAdd' (OppositeShift C A) a b (a + b) ⋯).hom.app X = ((shiftFunctorAdd' C a b (a + b) ⋯).inv.app (Opposite.unop X)).op
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : MulOneClass G<VAR>g : G<VAR>r : k<GOAL>r • (of k G) g = single g r
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : HasZeroObject C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : mk f = ⊥<GOAL>f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>LinearMap.ker (map R R A B) = Submodule.map (Finsupp.total A (Ω[A⁄R]) A ⇑(D R A)) (LinearMap.ker (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (Set.range (⇑(Finsupp.total A (Ω[A⁄R]) A ⇑(D R A)) ∘ fun x => Finsupp.single ((algebraMap R A) x) 1)) ⊔ Submodule.map (Finsupp.total A (Ω[A⁄R]) A ⇑(D R A)) (LinearMap.ker (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B))) = Submodule.map (Finsupp.total A (Ω[A⁄R]) A ⇑(D R A)) (LinearMap.ker (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (Set.range (⇑(Finsupp.total A (Ω[A⁄R]) A ⇑(D R A)) ∘ fun x => Finsupp.single ((algebraMap R A) x) 1)) = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>OrderBot (Submodule A (Ω[A⁄R]))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>∀ x ∈ Set.range (⇑(Finsupp.total A (Ω[A⁄R]) A ⇑(D R A)) ∘ fun x => Finsupp.single ((algebraMap R A) x) 1), x = 0
<VAR>a b c : ℕ<VAR>hac : a.Coprime c<VAR>b_dvd_c : b ∣ c<GOAL>(a * b).gcd c = b
<VAR>a b d : ℕ<VAR>hac : a.Coprime (d * b)<VAR>b_dvd_c : b ∣ d * b<GOAL>(a * b).gcd (d * b) = b
<VAR>a b d : ℕ<VAR>hac : a.Coprime (d * b)<VAR>b_dvd_c : b ∣ d * b<GOAL>a.gcd d * b = b
<VAR>a b d : ℕ<VAR>hac : a.Coprime (d * b)<VAR>b_dvd_c : b ∣ d * b<GOAL>a.gcd d = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝³ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝² : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>inst✝¹ : MulOneClass M'<VAR>inst✝ : MulOneClass N'<VAR>f : M →* N<VAR>g : M' →* N'<GOAL>mker (f.prodMap g) = (mker f).prod (mker g)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>inst✝ : Algebra.IsSeparable K L<VAR>b : Basis ι K L<GOAL>discr K ⇑b ≠ 0
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>inst✝ : Algebra.IsSeparable K L<VAR>b : Basis ι K L<GOAL>(traceForm K L).Nondegenerate
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)