Loading collection data...
Collections are a way for you to organize kata so that you can create your own training routines. Every collection you create is public and automatically sharable with other warriors. After you have added a few kata to a collection you and others can train on the kata contained within the collection.
Get started now by creating a new collection.
Regarding your comment in Preloaded:
Codewars currently uses Lean 3.39.1 with mathlib on commit fb41da97816e716c002c723f7f08e103874d9f50 from 10th February 2022.
This section about complex polarization identity was added in 19534b293505f3c23a01314e7c7fe4c11d06875c on 17th February 2022 so it didn't make it into the CW version.