Zulip Chat Archive

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
      use [0, 0],
      exact tensor_product.zero_tmul M 0,
      intros m n,
      use [m, n],
      rintros x y m₁, n₁, h₁ m₂, n₂, h₂⟩,
      rw [h₁, h₂],
      exact h m₁ m₂ n₁ n₂,
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