Commit 2025-04-28 10:53 91299a5d
View on Github →feat(RingTheory): tensor product of l.i. families over domains (#24224) There are also different conditions where the result is true. But I have yet to find a more general statement that encompasses all these results. See #24219 or https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Tensor.20product.20of.20linearly.20independent.20families/near/513258021