Commit 2024-10-30 11:48 89e654a3

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.