Similar theorems in different files with same name

Stream: mathlib4

[Maxwell Thum]

In Algebra.GCDMonoid.Basic, there is a theorem

@[simp]
theorem lcm_eq_zero_iff [GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0

In Algebra.GCDMonoid.Multiset, there is a generalization of that theorem

@[simp]
theorem lcm_eq_zero_iff [Nontrivial α] (s : Multiset α) : s.lcm = 0 ↔ (0 : α) ∈ s

whose proof uses the aforementioned lcm_eq_zero_iff.

[Maxwell Thum]

My issue is that when I try to simp using the first lcm_eq_zero_iff in the proof of the second, Lean thinks I'm referring to the second one (which I'm trying to prove!)

[Maxwell Thum]

And I can't figure out how to make Lean refer to the correct one

[Johan Commelin]

@Maxwell Thum Either add nonrec before the theorem keyword, or use _root_.lcm_eq_zero_iff.

[Maxwell Thum]

Johan Commelin said:

Maxwell Thum Either add nonrec before the theorem keyword, or use _root_.lcm_eq_zero_iff.

I think that works; thanks!