Commit 2023-01-05 03:18 fea26348
View on Github →feat: synchronize with mathlib3 #17905 (#1280) mathlib3 SHA: 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
[mathlib#17905](https://github.com/leanprover-community/mathlib/pull/17905/files#diff-deb01ba12632f4703c3dc29a10a34bd3a7d2a1c02dcf8b44d3e561fe3bde06fe) has been approved, so I think reviewers don't need to check the mathematical content.