# Commit 2024-10-30 11:48 89e654a3

View on Github →refactor: ungeneralize `LinearIndependent`

(#18426)
The existing definition is nonsense over semirings; this replaces it with a more plausible one, such that:

```
example : ¬ LinearIndependent ℕ Nat.succ := by
intro h
have := @h (.single 3 1) (.single 1 2)
simp [Finsupp.single_eq_single_iff] at this
```

which was previously true without the `¬`

.
Some of the nonsense semiring results following the definition must then be ungeneralized to rings.
I've been conservative here and only generalized the ones that generalizer trivially, and are used by important downstream
applications such as `Basis`

on semirings. Unimportant downstream applications have instead been ungeneralized to `Ring`

.
Many more results can likely be generalized in future.
Some context at https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20.60E.2FL.2FF.60.20and.20.60K.2FL'.2FF.60.20isomorphic.20.3D.3E.20.60.5BE.3AL.5D.3D.5BK.3AL'.5D.60/near/408999160.