mathlib3

9d86dad0 - feat(linear_algebra/prod): lemmas about ker and range (#8989)