PR !4#21342: refactor(Normed/Group/Quotient): generalise ...

Stream: triage

[Random Issue Bot]

Today I chose PR #21342 for discussion!

refactor(Normed/Group/Quotient): generalise to non-abelian groups
Created by @Yaël Dillies (@YaelDillies) on 2025-02-02
Labels: WIP, t-analysis

Is this PR still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

Relevant, currently stuck on working out how to rescue the existing proofs to the noncomp case