feat(data/prod): bijectivity of prod.map (#18446)
I needed this for showing a statement about invertibility of a map built with `linear_map.prod_map` (aka a "block diagonal" linear map), where the `nonempty` conditions are trivially true.
Forward-port will be at https://github.com/leanprover-community/mathlib4/pull/2346
