case inl
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : f = 1
⊢ ∑ g : G, ↑f g = ↑(Fintype.card G)

case inr
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, ↑f g = ↑0
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
⊢ ∑ g : G, ↑f g = ↑(if f = 1 then Fintype.card G else 0)
split_ifs with h
no goals
case inl
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : f = 1
⊢ ∑ g : G, ↑f g = ↑(Fintype.card G)
simp [h, card_univ]
case inr
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, ↑f g = 0
case inr
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, ↑f g = ↑0
rw [cast_zero]
no goals
case inr
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, ↑f g = 0
exact sum_hom_units_eq_zero f h