feat: definition and basic properties of linearly disjoint

[acmepjz]

---

• [ ] depends on: #12434 [part one: submodule version]
  • [x] depends on: #11635
  • [x] depends on: #11598 [need finsuppTensorFinsupp'_symm_single]
  • [x] depends on: #11731
  • [x] depends on: #11748
  • [x] depends on: #11859
• Subalgebra version:
  • [x] depends on: #12025
  • [ ] depends on: #12076
  • [x] depends on: #9626
  • [ ] depends on: #12846
  • [x] depends on: #12847
  • [x] depends on: #12849