mathlib3
d9edeea2 - refactor(linear_algebra/orientation): add refl, symm, and trans lemma (#10753)

Commit
4 years ago
refactor(linear_algebra/orientation): add refl, symm, and trans lemma (#10753) This restates the `reflexive`, `symmetric`, and `transitive` lemmas in a form understood by `@[refl]`, `@[symm]`, and `@[trans]`. As a bonus, these versions also work with dot notation. I've discarded the original statements, since they're always recoverable via the fields of equivalence_same_ray, and keeping them is just noise.
Author
Parents
Loading