R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ multiplicity ↑p ↑(x ^ n + y ^ n) = multiplicity ↑p ↑(x + y) + multiplicity p n
R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ multiplicity p (x ^ n + y ^ n) = multiplicity p (x + y) + multiplicity p n
iterate 2 rw [← Int.coe_nat_multiplicity]
R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑(x + y)
hx : ¬↑p ∣ ↑x
n : ℕ
hn : Odd n
⊢ multiplicity ↑p ↑(x ^ n + y ^ n) = multiplicity ↑p ↑(x + y) + multiplicity p n
R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ multiplicity ↑p ↑(x ^ n + y ^ n) = multiplicity ↑p ↑(x + y) + multiplicity p n
rw [← Int.coe_nat_dvd] at hxy hx
R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hx : ¬↑p ∣ ↑x
n : ℕ
hn : Odd n
hxy : ↑p ∣ ↑x + ↑y
⊢ multiplicity (↑p) (↑x ^ n + ↑y ^ n) = multiplicity (↑p) (↑x + ↑y) + multiplicity p n
R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑(x + y)
hx : ¬↑p ∣ ↑x
n : ℕ
hn : Odd n
⊢ multiplicity ↑p ↑(x ^ n + y ^ n) = multiplicity ↑p ↑(x + y) + multiplicity p n
push_cast at *
no goals
R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hx : ¬↑p ∣ ↑x
n : ℕ
hn : Odd n
hxy : ↑p ∣ ↑x + ↑y
⊢ multiplicity (↑p) (↑x ^ n + ↑y ^ n) = multiplicity (↑p) (↑x + ↑y) + multiplicity p n
exact Int.pow_add_pow hp hp1 hxy hx hn
R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ multiplicity ↑p ↑(x ^ n + y ^ n) = multiplicity ↑p ↑(x + y) + multiplicity p n
R : Type ?u.840239
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ multiplicity ↑p ↑(x ^ n + y ^ n) = multiplicity p (x + y) + multiplicity p n
rw [← Int.coe_nat_multiplicity]