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.

Estimated changes