mathlib

dc17b6ac - feat(algebra, linear_algebra): unique instances over the trivial ring (#18160)

feat(algebra, linear_algebra): unique instances over the trivial ring (#18160) Also generalizes module.subsingleton to mul_action_with_zero. matches https://github.com/leanprover-community/mathlib4/pull/1519