M : Type ?u.251015
A : Type u_1
B : Type ?u.251021
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ↑(↑(multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y
M : Type ?u.251015
A : Type u_1
B : Type ?u.251021
inst✝ : AddMonoid A
x y : A
⊢ y ∈ closure {x} ↔ ∃ n, n • x = y
rw [closure_singleton_eq, AddMonoidHom.mem_mrange]
no goals
M : Type ?u.251015
A : Type u_1
B : Type ?u.251021
inst✝ : AddMonoid A
x y : A
⊢ (∃ x_1, ↑(↑(multiplesHom A) x) x_1 = y) ↔ ∃ n, n • x = y
rfl