mathlib3
c062d9ea - feat(*): more bundled versions of `(fin 2 → α) ≃ (α × α)` (#10214)

Commit

4 years ago

feat(*): more bundled versions of `(fin 2 → α) ≃ (α × α)` (#10214) Also ensure that the inverse function uses vector notation when possible.

Author

urkud

Parents