case a
p : ℕ
R : Type u_1
S : Type ?u.87208
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ ↑ghostMap (teichmullerFun p (x * y)) = ↑ghostMap (teichmullerFun p x * teichmullerFun p y)
p : ℕ
R : Type u_1
S : Type ?u.87208
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
apply (ghostMap.bijective_of_invertible p (MvPolynomial R ℚ)).1
case a
p : ℕ
R : Type u_1
S : Type ?u.87208
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ ↑ghostMap (teichmullerFun p (x * y)) = ↑ghostMap (teichmullerFun p x) * ↑ghostMap (teichmullerFun p y)
case a
p : ℕ
R : Type u_1
S : Type ?u.87208
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ ↑ghostMap (teichmullerFun p (x * y)) = ↑ghostMap (teichmullerFun p x * teichmullerFun p y)
rw [RingHom.map_mul]
case a.h
p : ℕ
R : Type u_1
S : Type ?u.87208
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
n : ℕ
⊢ ↑ghostMap (teichmullerFun p (x * y)) n = (↑ghostMap (teichmullerFun p x) * ↑ghostMap (teichmullerFun p y)) n
case a
p : ℕ
R : Type u_1
S : Type ?u.87208
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
⊢ ↑ghostMap (teichmullerFun p (x * y)) = ↑ghostMap (teichmullerFun p x) * ↑ghostMap (teichmullerFun p y)
ext1 n
no goals
case a.h
p : ℕ
R : Type u_1
S : Type ?u.87208
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℚ
n : ℕ
⊢ ↑ghostMap (teichmullerFun p (x * y)) n = (↑ghostMap (teichmullerFun p x) * ↑ghostMap (teichmullerFun p y)) n
simp only [Pi.mul_apply, ghostMap_apply, ghostComponent_teichmullerFun, mul_pow]