Commit 2026-05-29 16:06 54898736

feat: another version of the cardinality of the difference (#37541) In mathlib there is Set.ncard_diff which states that (t \ s).ncard = t.ncard - s.ncard when s ⊆ t and s is finite. But one way to prove that s is finite is by showing that t is finite and using the s ⊆ t hypothesis, so this PR adds Set.ncard_diff' which assumes that t is finite instead of s.