mathlib
8f9f5ca0 - chore(linear_algebra/alternating): Use `have` instead of `simp only` (#5618)

Commit

5 years ago

chore(linear_algebra/alternating): Use `have` instead of `simp only` (#5618) This makes the proof easier to read and less fragile to lemma changes.

Author

eric-wieser

Parents