mathlib
dc0fadda - feat(linear_algebra/prod): define the graph of a linear map (#14266)

Commit

3 years ago

feat(linear_algebra/prod): define the graph of a linear map (#14266)

Author

ADedecker

ADedecker

Parents

Loading