mathlib

018309f0 - chore(linear_algebra/basis): replace explicit arguments for 0 ≠ 1 with nontrivial R (#3678)