Commit 2022-11-17 18:45 46129a8f
View on Github →feat: port data.char (#609) mathlib3 SHA: aab56fd783b265168f660d6b46709961153c4c20 Note: This file already existed in Mathlib4, so the material from mathlib3 was just added, but didn't replace the existing results.