Commit 2023-02-27 17:04 daa9ead4
View on Github →feat: forward-port leanprover-community/mathlib#18356 (#2000) This is the corresponding forward porting PR to https://github.com/leanprover-community/mathlib/pull/18356 and https://github.com/leanprover-community/mathlib/pull/18491