mathlib

292216d1 - Make connection `matrix.has_one ↔ pi.single` explicit, golf