no goals
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
⊢ IsNontrivial χ ↔ χ ≠ 1
simp only [IsNontrivial, Ne.def, ext_iff, not_forall, one_apply_coe]