case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
n : ℕ
⊢ χ ^ (2 * n + 1) = χ
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
n : ℕ
hn : Odd n
⊢ χ ^ n = χ
obtain ⟨n, rfl⟩ := hn
no goals
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
n : ℕ
⊢ χ ^ (2 * n + 1) = χ
rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]