F : Type ?u.74464
α : Type u_1
β : Type ?u.74470
R : Type ?u.74473
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Even m
a : ℕ
x✝ : a + 1 ≠ 0
⊢ Even (m * m ^ a)
F : Type ?u.74464
α : Type u_1
β : Type ?u.74470
R : Type ?u.74473
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Even m
a : ℕ
x✝ : a + 1 ≠ 0
⊢ Even (m ^ (a + 1))
rw [pow_succ]
no goals
F : Type ?u.74464
α : Type u_1
β : Type ?u.74470
R : Type ?u.74473
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Even m
a : ℕ
x✝ : a + 1 ≠ 0
⊢ Even (m * m ^ a)
exact hm.mul_right _