R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
f : R' →+* R''
a : R
⊢ ↑(ringHomComp χ f) a = 0 ∨ ↑(ringHomComp χ f) a = 1 ∨ ↑(ringHomComp χ f) a = -1
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
f : R' →+* R''
⊢ IsQuadratic (ringHomComp χ f)
intro a
no goals
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
f : R' →+* R''
a : R
⊢ ↑(ringHomComp χ f) a = 0 ∨ ↑(ringHomComp χ f) a = 1 ∨ ↑(ringHomComp χ f) a = -1
rcases hχ a with (ha | ha | ha) <;> simp [ha]