## Stream: new members

### Topic: What to do with small, self-contained lemmas?

#### Calvin Lee (Dec 17 2022 at 07:44):

Hello! I'm working on some localized module proofs that I'd like to upstream into mathlib. In particular that a localized module is a tensor product, which I just finished.
However, I'm not sure if all of the dependencies of my proofs should be upstreamed. For example, I wrote this small lemma about certain tensor products (they also occur if N is a cyclic group) that I'm not sure would be useful to others. Should I try to inline it into my proof? or make it private somehow within the file?
This is the lemma:

section tensor_product
variables {R M N : Type*} [comm_semiring R]  [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N]
lemma tensor_product.every_element_pure_if_absorbing_add
(x : tensor_product R M N) (h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), (∃ m n, m₁ ⊗ₜ n₁ + m₂ ⊗ₜ n₂ = m ⊗ₜ[R] n)) : (∃ m n, x = m ⊗ₜ n) :=
tensor_product.induction_on x
begin
use [0, 0],
symmetry,
exact tensor_product.zero_tmul M 0,
end
begin
intros m n,
use [m, n],
end
begin
rintros x y ⟨m₁, n₁, h₁⟩ ⟨m₂, n₂, h₂⟩,
rw [h₁, h₂],
exact h m₁ m₂ n₁ n₂,
end
end tensor_product


#### Kevin Buzzard (Dec 17 2022 at 09:07):

More smaller proofs is always better than fewer larger ones, surely!

#### Kevin Buzzard (Dec 17 2022 at 09:09):

That proof looks so golfable :-)

Last updated: Dec 20 2023 at 11:08 UTC