∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'],
  Module.annihilator R (M × M') = Module.annihilator R M ⊓ Module.annihilator R M'