symmDiff notation

Stream: mathlib4

[Eric Wieser]

Yaël Dillies said:

I guess adoption is slow here, and even slower since Patrick scoped the notation...

Didn't we revert that scoping once it was made clear that the symbol used was not just a capital delta?

[Yaël Dillies]

No

[Yaël Dillies]

In fact someone is trying to define symmDiff on Subgraph just now (see #14976), and I wonder whether that's not because the notation is missing

[Yaël Dillies]

cc @Pim Otte

[Pim Otte]

I think the reason for me is that nothing within SimpleGraph used it yet and I probably falsely rejected the one in Order as "not applicable".

[Yury G. Kudryashov]

(deleted)

[Notification Bot]

6 messages were moved here from #mathlib4 > (simp) normal forms for expressions about Filters by Eric Wieser.