mathlib
dc732a3c - feat(logic/basic): When an If-Then-Else is not one of its arguments (#10800)

Commit

4 years ago

feat(logic/basic): When an If-Then-Else is not one of its arguments (#10800) Conditions for `ite P a b ≠ a` and `ite P a b ≠ b`.

Author

YaelDillies

Parents