mathlib3
ef9d00f7 - feat(linear_algebra/matrix): multiplying `is_basis.to_matrix` and `linear_map.to_matrix` (#4650)

Commit

5 years ago

feat(linear_algebra/matrix): multiplying `is_basis.to_matrix` and `linear_map.to_matrix` (#4650) This basically tells us that `is_basis.to_matrix` is indeed a basis change matrix.

References

#4925 - Make prime-avoidance branch build

Author

Vierkantor

Parents

47dcecd2

mathlib3 ef9d00f7 - feat(linear_algebra/matrix): multiplying `is_basis.to_matrix` and `linear_map.to_matrix` (#4650)

mathlib3
ef9d00f7 - feat(linear_algebra/matrix): multiplying `is_basis.to_matrix` and `linear_map.to_matrix` (#4650)