mathlib3
chore(topology/algebra/module/basic): golf using injective APIs
#12676
Open
Open