Commit 2020-10-08 15:41 e74bd261

chore(*): add a few more unique instances (#4511)

• linear_map.unique_of_left, linear_map.unique_of_right, continuous_linear_map.unique_of_left, continuous_linear_map.unique_of_right: if either M or M₂ is a subsingleton, then both M →ₗ[R] M₂ and M →L[R] M₂ are unique;
• pi.unique: if each β a is unique, then Π a, β a is unique;
• rename function.injective.comap_subsingleton to function.injective.subsingleton;
• add unique.mk' and function.injective.unique;
• add a few simp lemmas for default;
• drop nonempty_unique_or_exists_ne and subsingleton_or_exists_ne;
• rename linear_map.coe_inj to coe_injective and continuous_linear_map.coe_inj to coe_fn_injective, make them use function.injective. Motivated by #4407