Commit 2022-12-29 14:17 0835141b
View on Github →feat : port Algebra.Regular.Pow (#1248)
Maybe I was lucky with my first port to mathlib4 or maybe I missed everything since no changes at all (except replacing Mathbin by Mathlib) were necessary for this port.
I must have done something wrong though since CI is failing in the check import phase and I don't know how to fix it.
Ok, I found out I need to add the file to Mathlib.lean....