α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
⊢ multiplicity a a = ↑1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
⊢ multiplicity a a = 1
rw [← Nat.cast_one]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
⊢ multiplicity a a = ↑1
exact eq_coe_iff.2 ⟨by simp, fun ⟨b, hb⟩ => ha (isUnit_iff_dvd_one.2
          ⟨b, mul_left_cancel₀ ha0 <| by simpa [_root_.pow_succ, mul_assoc] using hb⟩)⟩
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
⊢ a ^ 1 ∣ a
simp
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
x✝ : a ^ (1 + 1) ∣ a
b : α
hb : a = a ^ (1 + 1) * b
⊢ a * 1 = a * (a * b)
simpa [_root_.pow_succ, mul_assoc] using hb