α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a 1
⊢ 1 ∣ 1 ∧ ¬a ^ (0 + 1) ∣ 1
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a 1
⊢ Part.get (multiplicity a 1) ha = 0
rw [PartENat.get_eq_iff_eq_coe, eq_coe_iff, _root_.pow_zero]
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : Finite a 1
⊢ 1 ∣ 1 ∧ ¬a ^ (0 + 1) ∣ 1
simp [not_dvd_one_of_finite_one_right ha]