Commit 2026-09-03 09:19 5390e8a3

View on Github →

feat(Basic/IsEmpty): sigma types are empty when every fiber is empty (#43364) Add the instance Sigma.isEmpty_fibers, allowing us to simplify some proofs in ModelTheory.

Estimated changes