mathlib3
cd8fafa2 - chore(data/complex/module): split out orientation to a separate file (#18824)

Commit
2 years ago
chore(data/complex/module): split out orientation to a separate file (#18824) This removes the imports - linear_algebra.matrix.determinant - linear_algebra.matrix.mv_polynomial - linear_algebra.matrix.adjugate - linear_algebra.matrix.nonsingular_inverse - linear_algebra.matrix.basis - linear_algebra.determinant - linear_algebra.orientation from `data.complex.module`, which aren't otherwise needed here. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading