ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<GOAL>∀ (a : (CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) (Action.diagonal G n)).V), (Action.diagonalSucc G n).inv.hom a = (Equiv.piFinSuccAbove (fun a => G) 0).symm a
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<GOAL>∀ (a : (Action.diagonal G (n + 1)).V), (Action.diagonalSucc G n).hom.hom a = (Equiv.piFinSuccAbove (fun a => G) 0) a
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.LaxMonoidalFunctor V W<VAR>G : MonCat<GOAL>(CategoryTheory.MonoidalFunctor.mapActionLax F G).ε.hom = F.ε
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.LaxMonoidalFunctor V W<VAR>G : MonCat<GOAL>∀ (a : Action V G), ((CategoryTheory.MonoidalFunctor.mapActionLax F G).obj a).V = F.obj a.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.LaxMonoidalFunctor V W<VAR>G : MonCat<GOAL>∀ (a : Action V G) (g : ↑G), ((CategoryTheory.MonoidalFunctor.mapActionLax F G).obj a).ρ g = F.map (a.ρ g)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.LaxMonoidalFunctor V W<VAR>G : MonCat<VAR>X Y : Action V G<GOAL>((CategoryTheory.MonoidalFunctor.mapActionLax F G).μ X Y).hom = F.μ X.V Y.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.LaxMonoidalFunctor V W<VAR>G : MonCat<GOAL>∀ {X Y : Action V G} (a : X ⟶ Y), ((CategoryTheory.MonoidalFunctor.mapActionLax F G).map a).hom = F.map a.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.MonoidalFunctor V W<VAR>G : MonCat<GOAL>∀ (a : Action V G) (g : ↑G), ((F.mapAction G).obj a).ρ g = F.map (a.ρ g)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.MonoidalFunctor V W<VAR>G : MonCat<VAR>X Y : Action V G<GOAL>((F.mapAction G).μ X Y).hom = F.μ X.V Y.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.MonoidalFunctor V W<VAR>G : MonCat<GOAL>(F.mapAction G).ε.hom = F.ε
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.MonoidalFunctor V W<VAR>G : MonCat<GOAL>∀ {X Y : Action V G} (a : X ⟶ Y), ((F.mapAction G).map a).hom = F.map a.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.MonoidalFunctor V W<VAR>G : MonCat<GOAL>∀ (a : Action V G), ((F.mapAction G).obj a).V = F.obj a.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.MonoidalFunctor V W<VAR>G : MonCat<GOAL>(CategoryTheory.inv (F.mapAction G).ε).hom = CategoryTheory.inv F.ε
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.MonoidalCategory W<VAR>F : CategoryTheory.MonoidalFunctor V W<VAR>G : MonCat<VAR>X Y : Action V G<GOAL>(CategoryTheory.inv ((F.mapAction G).μ X Y)).hom = CategoryTheory.inv (F.μ X.V Y.V)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : ℕ<VAR>E : Fin n → Type u_2<VAR>(i : Fin n) → MeasureTheory.MeasureSpace (E i)<VAR>∀ (i : Fin n), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>f : (i : Fin n) → E i → 𝕜<VAR>hf : ∀ (i : Fin n), MeasureTheory.Integrable (f i) MeasureTheory.volume<GOAL>MeasureTheory.Integrable (fun x => ∏ i : Fin n, f i (x i)) MeasureTheory.volume
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>ι : Type u_2<VAR>Fintype ι<VAR>E : ι → Type u_3<VAR>f : (i : ι) → E i → 𝕜<VAR>(i : ι) → MeasureTheory.MeasureSpace (E i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>hf : ∀ (i : ι), MeasureTheory.Integrable (f i) MeasureTheory.volume<GOAL>MeasureTheory.Integrable (fun x => ∏ i : ι, f i (x i)) MeasureTheory.volume
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>ι : Type u_2<VAR>Fintype ι<VAR>E : Type u_3<VAR>f : ι → E → 𝕜<VAR>MeasureTheory.MeasureSpace E<VAR>MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>hf : ∀ (i : ι), MeasureTheory.Integrable (f i) MeasureTheory.volume<GOAL>MeasureTheory.Integrable (fun x => ∏ i : ι, f i (x i)) MeasureTheory.volume
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : ℕ<VAR>E : Fin n → Type u_2<VAR>(i : Fin n) → MeasureTheory.MeasureSpace (E i)<VAR>∀ (i : Fin n), MeasureTheory.SigmaFinite MeasureTheory.volume<VAR>f : (i : Fin n) → E i → 𝕜<GOAL>∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>ι : Type u_2<VAR>Fintype ι<VAR>E : ι → Type u_3<VAR>f : (i : ι) → E i → 𝕜<VAR>(i : ι) → MeasureTheory.MeasureSpace (E i)<VAR>∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume<GOAL>∫ (x : (i : ι) → E i), ∏ i : ι, f i (x i) = ∏ i : ι, ∫ (x : E i), f i x
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>Fintype ι<VAR>f : E → 𝕜<VAR>MeasureTheory.MeasureSpace E<VAR>MeasureTheory.SigmaFinite MeasureTheory.volume<GOAL>∫ (x : ι → E), ∏ i : ι, f (x i) = (∫ (x : E), f x) ^ Fintype.card ι
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>m : CoeSort.coe A<VAR>g : G<GOAL>(groupCohomology.dZero A) m g = (A.ρ g) m - m
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>LinearMap.ker (groupCohomology.dZero A) = A.ρ.invariants
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<GOAL>groupCohomology.dZero A = 0
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G → CoeSort.coe A<VAR>g : G × G<GOAL>(groupCohomology.dOne A) f g = (A.ρ g.1) (f g.2) - f (g.1 * g.2) + f g.1
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G × G → CoeSort.coe A<VAR>g : G × G × G<GOAL>(groupCohomology.dTwo A) f g = (A.ρ g.1) (f (g.2.1, g.2.2)) - f (g.1 * g.2.1, g.2.2) + f (g.1, g.2.1 * g.2.2) - f (g.1, g.2.1)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomology.dZero A ∘ₗ ↑(groupCohomology.zeroCochainsLequiv A) = ↑(groupCohomology.oneCochainsLequiv A) ∘ₗ (groupCohomology.inhomogeneousCochains A).d 0 1
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomology.dOne A ∘ₗ ↑(groupCohomology.oneCochainsLequiv A) = ↑(groupCohomology.twoCochainsLequiv A) ∘ₗ (groupCohomology.inhomogeneousCochains A).d 1 2
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomology.dTwo A ∘ₗ ↑(groupCohomology.twoCochainsLequiv A) = ↑(groupCohomology.threeCochainsLequiv A) ∘ₗ (groupCohomology.inhomogeneousCochains A).d 2 3
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomology.dOne A ∘ₗ groupCohomology.dZero A = 0
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomology.dTwo A ∘ₗ groupCohomology.dOne A = 0
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G → CoeSort.coe A<GOAL>f ∈ groupCohomology.oneCocycles A ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G → CoeSort.coe A<GOAL>f ∈ groupCohomology.oneCocycles A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : ↥(groupCohomology.oneCocycles A)<GOAL>↑f 1 = 0
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : ↥(groupCohomology.oneCocycles A)<VAR>g : G<GOAL>(A.ρ g) (↑f g⁻¹) = -↑f g
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<VAR>f : ↥(groupCohomology.oneCocycles A)<VAR>g h : G<GOAL>↑f (g * h) = ↑f g + ↑f h
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<VAR>f : Additive G →+ CoeSort.coe A<GOAL>⇑f ∘ ⇑Additive.ofMul ∈ groupCohomology.oneCocycles A
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>hA : A.IsTrivial<VAR>f : ↥(groupCohomology.oneCocycles A)<GOAL>∀ (a : Additive G), ((groupCohomology.oneCocyclesLequivOfIsTrivial A) f) a = (↑f ∘ ⇑Additive.toMul) a
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>hA : A.IsTrivial<VAR>f : Additive G →+ CoeSort.coe A<VAR>a : Additive G<GOAL>↑((groupCohomology.oneCocyclesLequivOfIsTrivial A).symm f) a = f a
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G × G → CoeSort.coe A<GOAL>f ∈ groupCohomology.twoCocycles A ↔ ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G × G → CoeSort.coe A<GOAL>f ∈ groupCohomology.twoCocycles A ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : ↥(groupCohomology.twoCocycles A)<VAR>g : G<GOAL>↑f (1, g) = ↑f (1, 1)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : ↥(groupCohomology.twoCocycles A)<VAR>g : G<GOAL>↑f (g, 1) = (A.ρ g) (↑f (1, 1))
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : ↥(groupCohomology.twoCocycles A)<VAR>g : G<GOAL>(A.ρ g) (↑f (g⁻¹, g)) - ↑f (g, g⁻¹) = ↑f (1, 1) - ↑f (g, 1)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G → CoeSort.coe A<VAR>h : f ∈ LinearMap.range (groupCohomology.dZero A)<GOAL>↑↑(groupCohomology.oneCoboundariesOfMemRange h) = f
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G → CoeSort.coe A<VAR>x : CoeSort.coe A<VAR>hf : ∀ (g : G), (A.ρ g) x - x = f g<GOAL>↑↑(groupCohomology.oneCoboundariesOfEq hf) = f
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : ↥(groupCohomology.oneCocycles A)<VAR>h : f ∈ groupCohomology.oneCoboundaries A<GOAL>↑f ∈ LinearMap.range (groupCohomology.dZero A)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<GOAL>groupCohomology.oneCoboundaries A = ⊥
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G × G → CoeSort.coe A<VAR>h : f ∈ LinearMap.range (groupCohomology.dOne A)<GOAL>↑↑(groupCohomology.twoCoboundariesOfMemRange h) = f
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : G × G → CoeSort.coe A<VAR>x : G → CoeSort.coe A<VAR>hf : ∀ (g h : G), (A.ρ g) (x h) - x (g * h) + x g = f (g, h)<GOAL>↑↑(groupCohomology.twoCoboundariesOfEq hf) = f
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>f : ↥(groupCohomology.twoCocycles A)<VAR>h : f ∈ groupCohomology.twoCoboundaries A<GOAL>(groupCohomology.twoCocycles A).subtype f ∈ LinearMap.range (groupCohomology.dOne A)
<VAR>G : Type u_1<VAR>A : Type u_2<VAR>Monoid G<VAR>AddCommGroup A<VAR>MulAction G A<VAR>f : G → A<VAR>hf : groupCohomology.IsOneCocycle f<GOAL>f 1 = 0
<VAR>G : Type u_1<VAR>A : Type u_2<VAR>Monoid G<VAR>AddCommGroup A<VAR>MulAction G A<VAR>f : G × G → A<VAR>hf : groupCohomology.IsTwoCocycle f<VAR>g : G<GOAL>f (1, g) = f (1, 1)
<VAR>G : Type u_1<VAR>A : Type u_2<VAR>Monoid G<VAR>AddCommGroup A<VAR>MulAction G A<VAR>f : G × G → A<VAR>hf : groupCohomology.IsTwoCocycle f<VAR>g : G<GOAL>f (g, 1) = g • f (1, 1)
<VAR>G : Type u_1<VAR>A : Type u_2<VAR>Group G<VAR>AddCommGroup A<VAR>MulAction G A<VAR>f : G → A<VAR>hf : groupCohomology.IsOneCocycle f<VAR>g : G<GOAL>g • f g⁻¹ = -f g
<VAR>G : Type u_1<VAR>A : Type u_2<VAR>Group G<VAR>AddCommGroup A<VAR>MulAction G A<VAR>f : G × G → A<VAR>hf : groupCohomology.IsTwoCocycle f<VAR>g : G<GOAL>g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
<VAR>k G A : Type u<VAR>CommRing k<VAR>Group G<VAR>AddCommGroup A<VAR>Module k A<VAR>DistribMulAction G A<VAR>SMulCommClass G k A<VAR>f : ↥(groupCohomology.oneCocycles (Rep.ofDistribMulAction k G A))<GOAL>groupCohomology.IsOneCocycle ↑f
<VAR>k G A : Type u<VAR>CommRing k<VAR>Group G<VAR>AddCommGroup A<VAR>Module k A<VAR>DistribMulAction G A<VAR>SMulCommClass G k A<VAR>f : ↥(groupCohomology.oneCoboundaries (Rep.ofDistribMulAction k G A))<GOAL>groupCohomology.IsOneCoboundary ↑↑f
<VAR>k G A : Type u<VAR>CommRing k<VAR>Group G<VAR>AddCommGroup A<VAR>Module k A<VAR>DistribMulAction G A<VAR>SMulCommClass G k A<VAR>f : ↥(groupCohomology.twoCocycles (Rep.ofDistribMulAction k G A))<GOAL>groupCohomology.IsTwoCocycle ↑f
<VAR>k G A : Type u<VAR>CommRing k<VAR>Group G<VAR>AddCommGroup A<VAR>Module k A<VAR>DistribMulAction G A<VAR>SMulCommClass G k A<VAR>f : ↥(groupCohomology.twoCoboundaries (Rep.ofDistribMulAction k G A))<GOAL>groupCohomology.IsTwoCoboundary ↑↑f
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>Monoid G<VAR>CommGroup M<VAR>MulAction G M<VAR>f : G → M<VAR>hf : groupCohomology.IsMulOneCocycle f<GOAL>f 1 = 1
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>Monoid G<VAR>CommGroup M<VAR>MulAction G M<VAR>f : G × G → M<VAR>hf : groupCohomology.IsMulTwoCocycle f<VAR>g : G<GOAL>f (1, g) = f (1, 1)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>Monoid G<VAR>CommGroup M<VAR>MulAction G M<VAR>f : G × G → M<VAR>hf : groupCohomology.IsMulTwoCocycle f<VAR>g : G<GOAL>f (g, 1) = g • f (1, 1)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>Group G<VAR>CommGroup M<VAR>MulAction G M<VAR>f : G → M<VAR>hf : groupCohomology.IsMulOneCocycle f<VAR>g : G<GOAL>g • f g⁻¹ = (f g)⁻¹
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>Group G<VAR>CommGroup M<VAR>MulAction G M<VAR>f : G × G → M<VAR>hf : groupCohomology.IsMulTwoCocycle f<VAR>g : G<GOAL>g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
<VAR>G M : Type<VAR>Group G<VAR>CommGroup M<VAR>MulDistribMulAction G M<VAR>f : ↥(groupCohomology.oneCocycles (Rep.ofMulDistribMulAction G M))<GOAL>groupCohomology.IsMulOneCocycle (⇑Additive.toMul ∘ ↑f)
<VAR>G M : Type<VAR>Group G<VAR>CommGroup M<VAR>MulDistribMulAction G M<VAR>f : ↥(groupCohomology.oneCoboundaries (Rep.ofMulDistribMulAction G M))<GOAL>groupCohomology.IsMulOneCoboundary (⇑Additive.ofMul ∘ ↑↑f)
<VAR>G M : Type<VAR>Group G<VAR>CommGroup M<VAR>MulDistribMulAction G M<VAR>f : ↥(groupCohomology.twoCocycles (Rep.ofMulDistribMulAction G M))<GOAL>groupCohomology.IsMulTwoCocycle (⇑Additive.toMul ∘ ↑f)
<VAR>G M : Type<VAR>Group G<VAR>CommGroup M<VAR>MulDistribMulAction G M<VAR>f : ↥(groupCohomology.twoCoboundaries (Rep.ofMulDistribMulAction G M))<GOAL>groupCohomology.IsMulTwoCoboundary (⇑Additive.toMul ∘ ↑↑f)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<GOAL>↑(groupCohomology.H0LequivOfIsTrivial A) = A.ρ.invariants.subtype
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<VAR>x : ↥(groupCohomology.H0 A)<GOAL>(groupCohomology.H0LequivOfIsTrivial A) x = ↑x
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<VAR>x : CoeSort.coe A<GOAL>↑((groupCohomology.H0LequivOfIsTrivial A).symm x) = x
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<GOAL>↑(groupCohomology.H1LequivOfIsTrivial A) ∘ₗ groupCohomology.H1_π A = ↑(groupCohomology.oneCocyclesLequivOfIsTrivial A)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<VAR>f : ↥(groupCohomology.oneCocycles A)<VAR>x : Additive G<GOAL>((groupCohomology.H1LequivOfIsTrivial A) ((groupCohomology.H1_π A) f)) x = ↑f (Additive.toMul x)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>A.IsTrivial<VAR>f : Additive G →+ CoeSort.coe A<GOAL>(groupCohomology.H1LequivOfIsTrivial A).symm f = (groupCohomology.H1_π A) ((groupCohomology.oneCocyclesLequivOfIsTrivial A).symm f)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomology.dZero A ∘ₗ (groupCohomology.H0 A).subtype = 0
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.shortComplexH0 A).Exact
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.dZeroArrowIso A).inv.right = ↑(groupCohomology.oneCochainsLequiv A).symm
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.dZeroArrowIso A).inv.left = ↑(groupCohomology.zeroCochainsLequiv A).symm
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.dZeroArrowIso A).hom.right = ↑(groupCohomology.oneCochainsLequiv A)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.dZeroArrowIso A).hom.left = ↑(groupCohomology.zeroCochainsLequiv A)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.isoZeroCocycles A).hom ≫ A.ρ.invariants.subtype = groupCohomology.iCocycles A 0 ≫ (groupCohomology.zeroCochainsLequiv A).toModuleIso.hom
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomologyπ A 0 ≫ (groupCohomology.isoH0 A).hom = (groupCohomology.isoZeroCocycles A).hom
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.shortComplexH1Iso A).inv = CategoryTheory.ShortComplex.homMk ↑(groupCohomology.zeroCochainsLequiv A).symm ↑(groupCohomology.oneCochainsLequiv A).symm ↑(groupCohomology.twoCochainsLequiv A).symm ⋯ ⋯
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.shortComplexH1Iso A).hom = { τ₁ := ↑(groupCohomology.zeroCochainsLequiv A), τ₂ := ↑(groupCohomology.oneCochainsLequiv A), τ₃ := ↑(groupCohomology.twoCochainsLequiv A), comm₁₂ := ⋯, comm₂₃ := ⋯ }
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.isoOneCocycles A).hom ≫ ModuleCat.ofHom (groupCohomology.oneCocycles A).subtype = groupCohomology.iCocycles A 1 ≫ (groupCohomology.oneCochainsLequiv A).toModuleIso.hom
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomology.toCocycles A 0 1 ≫ (groupCohomology.isoOneCocycles A).hom = (groupCohomology.zeroCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (groupCohomology.shortComplexH1 A).moduleCatToCycles
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomologyπ A 1 ≫ (groupCohomology.isoH1 A).hom = (groupCohomology.isoOneCocycles A).hom ≫ (groupCohomology.shortComplexH1 A).moduleCatHomologyπ
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.shortComplexH2Iso A).inv = CategoryTheory.ShortComplex.homMk ↑(groupCohomology.oneCochainsLequiv A).symm ↑(groupCohomology.twoCochainsLequiv A).symm ↑(groupCohomology.threeCochainsLequiv A).symm ⋯ ⋯
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.shortComplexH2Iso A).hom = { τ₁ := ↑(groupCohomology.oneCochainsLequiv A), τ₂ := ↑(groupCohomology.twoCochainsLequiv A), τ₃ := ↑(groupCohomology.threeCochainsLequiv A), comm₁₂ := ⋯, comm₂₃ := ⋯ }
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>(groupCohomology.isoTwoCocycles A).hom ≫ ModuleCat.ofHom (groupCohomology.twoCocycles A).subtype = groupCohomology.iCocycles A 2 ≫ (groupCohomology.twoCochainsLequiv A).toModuleIso.hom
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomology.toCocycles A 1 2 ≫ (groupCohomology.isoTwoCocycles A).hom = (groupCohomology.oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (groupCohomology.shortComplexH2 A).moduleCatToCycles
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<GOAL>groupCohomologyπ A 2 ≫ (groupCohomology.isoH2 A).hom = (groupCohomology.isoTwoCocycles A).hom ≫ (groupCohomology.shortComplexH2 A).moduleCatHomologyπ
<VAR>n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsCyclotomicExtension {n} A B<GOAL>IsPrimitiveRoot (IsCyclotomicExtension.zeta n A B) ↑n
<VAR>n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsCyclotomicExtension {n} A B<VAR>IsDomain B<VAR>NeZero ↑↑n<GOAL>(Polynomial.aeval (IsCyclotomicExtension.zeta n A B)) (Polynomial.cyclotomic (↑n) A) = 0
<VAR>n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsCyclotomicExtension {n} A B<VAR>IsDomain B<VAR>NeZero ↑↑n<GOAL>(Polynomial.cyclotomic (↑n) B).IsRoot (IsCyclotomicExtension.zeta n A B)
<VAR>n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsCyclotomicExtension {n} A B<GOAL>IsCyclotomicExtension.zeta n A B ^ ↑n = 1
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>(IsPrimitiveRoot.powerBasis K hζ).gen = ζ
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>(IsPrimitiveRoot.powerBasis K hζ).dim = (minpoly K ζ).natDegree
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>(IsPrimitiveRoot.powerBasis K hζ).gen ∈ Algebra.adjoin K {ζ - 1}
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>(IsPrimitiveRoot.subOnePowerBasis K hζ).dim = (minpoly K (ζ - 1)).natDegree
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>(IsPrimitiveRoot.subOnePowerBasis K hζ).gen = ζ - 1
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>C : Type u_1<VAR>CommRing C<VAR>IsDomain C<VAR>Algebra K C<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑n) K)<VAR>φ' : L →ₐ[K] C<GOAL>↑((hζ.embeddingsEquivPrimitiveRoots C hirr) φ') = φ' ζ
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>IsCyclotomicExtension {n} K L<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑n) K)<GOAL>FiniteDimensional.finrank K L = φ ↑n
<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>p q : ℕ<VAR>x y : L<VAR>hx : IsPrimitiveRoot x p<VAR>hy : IsPrimitiveRoot y q<VAR>hirr : Irreducible (Polynomial.cyclotomic (p.lcm q) K)<GOAL>φ (p.lcm q) ≤ FiniteDimensional.finrank K L
<VAR>n : ℕ+<VAR>K : Type u<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {n} ℚ K<VAR>ζ : K<VAR>l : ℕ<VAR>hζ : IsPrimitiveRoot ζ l<VAR>hl : l ≠ 0<GOAL>l ∣ 2 * ↑n
<VAR>n : ℕ+<VAR>K : Type u<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<GOAL>∃ r, x = (-ζ) ^ r
<VAR>n : ℕ+<VAR>K : Type u<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<GOAL>∃ r < ↑n, x = ζ ^ r ∨ x = -ζ ^ r
<VAR>K : Type u<VAR>L : Type v<VAR>CommRing L<VAR>ζ : L<VAR>Field K<VAR>Algebra K L<VAR>hζ : IsPrimitiveRoot ζ 2<VAR>IsDomain L<GOAL>(Algebra.norm K) ζ = (-1) ^ FiniteDimensional.finrank K L
<VAR>n : ℕ+<VAR>K : Type u<VAR>L : Type v<VAR>CommRing L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>Field K<VAR>Algebra K L<VAR>IsDomain L<VAR>IsCyclotomicExtension {n} K L<VAR>hn : n ≠ 2<VAR>hirr : Irreducible (Polynomial.cyclotomic (↑n) K)<GOAL>(Algebra.norm K) ζ = 1
<VAR>n : ℕ+<VAR>L : Type v<VAR>CommRing L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>Algebra K L<VAR>hodd : Odd ↑n<GOAL>(Algebra.norm K) ζ = 1