noncomputable def GroupCohomology.lemma_23_27 {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] (A : Rep.{u, u, u} k ↥⊥) : Rep.ind ⊥.subtype A ≅ Rep.coind.{u, u, u, u} ⊥.subtype A

noncomputable def GroupCohomology.lemma_23_27_natIso {k : Type u} [CommRing k] {G : Type u} [Group G] [Fintype G] : induced_def k G ≅ coinduced_def k G

@[reducible, inline]

noncomputable abbrev GroupCohomology.indCoindIso_bot {k : Type u_1} [CommRing k] {G : Type u_1} [Group G] [Fintype G] (A : Rep.{u_1, u_1, u_1} k ↥⊥) : Rep.ind ⊥.subtype A ≅ Rep.coind.{u_1, u_1, u_1, u_1} ⊥.subtype A

@[reducible, inline]

noncomputable abbrev GroupCohomology.indCoindNatIso_bot {k : Type u_1} [CommRing k] {G : Type u_1} [Group G] [Fintype G] : induced_def k G ≅ coinduced_def k G