GroupTheory.Coset !4#1874

Stream: mathlib4

[Johan Commelin]

Can someone who understands coes in Lean 4 give an indication on how to rewrite this library note:
https://github.com/leanprover-community/mathlib4/pull/1874/files#diff-acf3b28719621b199a00f9acc9f5f3fee2e1557bfd0cfabab6549f3301334e2aR892-R899

[Eric Wieser]

Not really relevant, but surely the times in the line above should be prod...

[Gabriel Ebner]

answered on github