no goals
α : Type u_1
β : Type ?u.209427
γ : Type ?u.209430
δ : Type ?u.209433
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
x✝ : IsUnit q
v : αˣ
hv : ↑v = q
⊢ ↑(v * u⁻¹) = p
simp [hv, hu.symm]
α : Type u_1
β : Type ?u.209427
γ : Type ?u.209430
δ : Type ?u.209433
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
⊢ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
α : Type u_1
β : Type ?u.209427
γ : Type ?u.209430
δ : Type ?u.209433
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
⊢ ∀ (a b : α), p * ↑u ∣ a * b → p * ↑u ∣ a ∨ p * ↑u ∣ b
simp [Units.mul_right_dvd]
α : Type u_1
β : Type ?u.209427
γ : Type ?u.209430
δ : Type ?u.209433
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
a b : α
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b
α : Type u_1
β : Type ?u.209427
γ : Type ?u.209430
δ : Type ?u.209433
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
⊢ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
intro a b
no goals
α : Type u_1
β : Type ?u.209427
γ : Type ?u.209430
δ : Type ?u.209433
inst✝ : CommMonoidWithZero α
p q : α
h : p ~ᵤ q
hp : Prime p
u : αˣ
hu : p * ↑u = q
a b : α
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b
exact hp.dvd_or_dvd