@[implicit_reducible]

noncomputable instance TateCohomology.tateH0.inhabited {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Inhabited (tateH0 A)

@[implicit_reducible]

instance TateCohomology.tateMinus1.inhabited {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) : Inhabited (tateMinus1 A)

theorem TateCohomology.herbrandQuotient_eq_one_of_finite' {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] [IsCyclic G] (A : Rep.{u, u, u} k G) [Finite ↑A] [Fintype (tateH0 A)] [Fintype (tateMinus1 A)] : herbrandQuotient A = 1

instance TateCohomology.tateH0.finite {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) [Finite ↑A] : Finite (tateH0 A)

instance TateCohomology.tateMinus1.finite {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k G) [Finite ↑A] : Finite (tateMinus1 A)

theorem TateCohomology.finite_of_shortExact_torsion_fg {G₀ : Type} [Group G₀] [Fintype G₀] {S : CategoryTheory.ShortComplex (Rep.{u_1, 0, 0} ℤ G₀)} (hS : S.ShortExact) (htors : Module.IsTorsion ℤ ↑S.X₁) (hfg : Module.Finite ℤ ↑S.X₂) : Finite ↑S.X₁

theorem TateCohomology.herbrandQuotient_eq_shortExact_torsion {G₀ : Type} [Group G₀] [Fintype G₀] [IsCyclic G₀] {S : CategoryTheory.ShortComplex (Rep.{0, 0, 0} ℤ G₀)} (hS : S.ShortExact) (htors : Module.IsTorsion ℤ ↑S.X₁) (hfg : Module.Finite ℤ ↑S.X₂) [Fintype (tateH0 S.X₂)] [Fintype (tateMinus1 S.X₂)] [Fintype (tateH0 S.X₃)] [Fintype (tateMinus1 S.X₃)] : herbrandQuotient S.X₂ = herbrandQuotient S.X₃

theorem TateCohomology.herbrandQuotient_trivial_pow_clean {G₀ : Type} [Group G₀] [Fintype G₀] [IsCyclic G₀] (M : Type) [AddCommGroup M] [Module.Finite ℤ M] [Fintype (tateH0 (Rep.trivial ℤ G₀ M))] [Fintype (tateMinus1 (Rep.trivial ℤ G₀ M))] : herbrandQuotient (Rep.trivial ℤ G₀ M) = ↑(Fintype.card G₀) ^ Module.finrank ℤ M