Commit 2025-02-27 18:30 908e1733
View on Github →feat: a condition for two indicators to be equal (#22329)
If f a = g b, then to prove s.mulIndicator f a = t.mulIndicator g b it is enough to prove a ∈ s ↔ b ∈ t.
feat: a condition for two indicators to be equal (#22329)
If f a = g b, then to prove s.mulIndicator f a = t.mulIndicator g b it is enough to prove a ∈ s ↔ b ∈ t.