α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
⊢ count p (factors m) ≠ 0 → p ≤ m
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
⊢ count p (factors m) ≠ 0 → p ≤ m
nontriviality α
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
⊢ 0 < count p (factors m) → p ≤ m
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
⊢ count p (factors m) ≠ 0 → p ≤ m
rw [← pos_iff_ne_zero]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
h : 0 < count p (factors m)
⊢ p ≤ m
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
⊢ 0 < count p (factors m) → p ≤ m
intro h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
h : 0 < count p (factors m)
⊢ p ^ 1 ≤ m
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
h : 0 < count p (factors m)
⊢ p ≤ m
rw [← pow_one p]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
h : 0 < count p (factors m)
⊢ 1 ≤ count p (factors m)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
h : 0 < count p (factors m)
⊢ p ^ 1 ≤ m
apply (prime_pow_dvd_iff_le h0 hp).2
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
✝ : Nontrivial α
h : 0 < count p (factors m)
⊢ 1 ≤ count p (factors m)
simpa only