F : Type ?u.91525
α : Type u_1
β : Type ?u.91531
R : Type ?u.91534
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
⊢ Odd 1
F : Type ?u.91525
α : Type u_1
β : Type ?u.91531
R : Type ?u.91534
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
⊢ Odd (m ^ 0)
rw [pow_zero]
no goals
F : Type ?u.91525
α : Type u_1
β : Type ?u.91531
R : Type ?u.91534
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
⊢ Odd 1
exact odd_one
F : Type ?u.91525
α : Type u_1
β : Type ?u.91531
R : Type ?u.91534
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
a : ℕ
⊢ Odd (m * m ^ a)
F : Type ?u.91525
α : Type u_1
β : Type ?u.91531
R : Type ?u.91534
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
a : ℕ
⊢ Odd (m ^ (a + 1))
rw [pow_succ]
no goals
F : Type ?u.91525
α : Type u_1
β : Type ?u.91531
R : Type ?u.91534
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
a : ℕ
⊢ Odd (m * m ^ a)
exact hm.mul <| Odd.pow hm