no goals
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ a ^ 0 ∣ b
simp only [_root_.pow_zero, one_dvd]
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ ¬a ∣ b
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ ¬a ^ (0 + 1) ∣ b
rw [pow_one]
no goals
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
ha : ¬IsUnit a
hb : IsUnit b
⊢ ¬a ∣ b
exact fun h => mt (isUnit_of_dvd_unit h) ha hb