mathlib
94a4a958 - feat(logic/basic): `is_trans Prop iff` instance (#6836)

Commit

5 years ago

feat(logic/basic): `is_trans Prop iff` instance (#6836) If you've ever wondered why `trans h1 h2` works for `≤` but not for `↔`, this is the reason.

Author

gebner

Parents