On the coherence of one-relator groups and their group algebras

Problem statement

Notes: Unavailable.

Source: A. Jaikin-Zapirain and M. Linton, `On the coherence of one-relator groups and their group algebras`, Annals of Math, 201 (3) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2025-201-3-OnCoherenceOfOneRelatorGroups.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 (G K : Type*) [Group G] [Field K] [CharZero K] (hG : Group.OneRelator G) :
    Group.Coherent G ∧ Ring.Coherent (MonoidAlgebra K G) := byG:Type u_1K:Type u_2inst✝²:Group Ginst✝¹:Field Kinst✝:CharZero KhG:Group.OneRelator G⊢ Group.Coherent G ∧ Ring.Coherent (MonoidAlgebra K G)
  sorryAll goals completed! 🐙