Commit 2024-05-26 12:33 16a1db9e
View on Github →fix: align Set.empty_def with mathlib3 (#13218) During the port, a coercion to type slipped in where there was none in mathlib3.
fix: align Set.empty_def with mathlib3 (#13218) During the port, a coercion to type slipped in where there was none in mathlib3.