Theorem Module.Free.of_subsingleton'

Modification history

2025-07-31 17:11
Mathlib/LinearAlgebra/FreeModule/Basic.lean
chore: scope or remove some instances (#27592) …
Added Module.Free.of_subsingleton'View on Github →