Commit 2024-02-25 23:46 40aaad72

chore: generalize more DirectSum results to avoid negation (#10965) Generalize Basis.tensorProduct and instance Module.Free.tensor to CommSemiring and AddCommMonoid, as a follow-up to #10828. Plus style fixes:

• tidy up LinearAlgebra.DirectSum.Finsupp.lean:
  • delete unused universe declaration
  • delete duplicate open TensorProduct
  • delete redundant noncomputable annotation and associated comment (due to noncomputable section in the same file)
  • use variable
• delete "typeclass reminders" in "Module.Flat.iff_rTensor_injective'" (no longer needed)
• whitespace fixes
• simplify file structure (section/namespace/open/variable)