case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ∑ a : R, ↑χ a = 0
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsNontrivial χ
⊢ ∑ a : R, ↑χ a = 0
rcases hχ with ⟨b, hb⟩
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ↑χ ↑b * ∑ a : R, ↑χ a = ∑ a : R, ↑χ a
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ∑ a : R, ↑χ a = 0
refine' eq_zero_of_mul_eq_self_left hb _
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ∑ x : R, ↑χ ↑b * ↑χ x = ∑ a : R, ↑χ a
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ↑χ ↑b * ∑ a : R, ↑χ a = ∑ a : R, ↑χ a
simp only [Finset.mul_sum, ← map_mul]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
x : R
⊢ ↑χ ↑b * ↑χ x = ↑χ (↑b * x)
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ∑ x : R, ↑χ ↑b * ↑χ x = ∑ a : R, ↑χ a
refine Fintype.sum_bijective _ (Units.mulLeft_bijective b) _ _ fun x => ?_
no goals
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
x : R
⊢ ↑χ ↑b * ↑χ x = ↑χ (↑b * x)
exact (map_mul χ (b : R) x).symm