Sum of a multiplicative subgroup of a field is zero

Stream: Is there code for X?

[Bolton Bailey]

Do we have anywhere the statement that the sum of a nontrivial multiplicative subgroup of a field is zero?

[Adam Topaz]

Do we know that finite subgroups of multiplicative groups of fields are cyclic? I don’t recall seeing such statements in mathlib

[Eric Wieser]

So (H : subgroup Fˣ) : H ≠ ⊥ → ∑ᶠ x ∈ H, (x : F) = 0?

[Bolton Bailey]

Excuse me for not being familiar with the ∑ᶠ notation, I'm only really interested in fields that are already finite, but that looks right

[Eric Wieser]

Ah, I assumed otherwise since you didn't mention finiteness

[Bolton Bailey]

Well at first I thought it was only true of finite fields, but I realized the proof in my head doesn't need finiteness of the field itself as long as the subgroup is finite

[Adam Topaz]

It’s true in general

[Adam Topaz]

(For finite subgroups, or with the sum^f that Eric mentioned in general)

[Eric Wieser]

And also for tsum?

[Adam Topaz]

docs#tsum

[Adam Topaz]

No

[Adam Topaz]

Well I don’t think so.

[Adam Topaz]

Finiteness is key in the proof I know

[Yaël Dillies]

But if it's infinite then the sum is zero by junk value, right?

[Adam Topaz]

Yes, but not for tsum

[Bolton Bailey]

Is there an example where the tsum is of an infinite multiplicative subgroup but exists?

[Yaël Dillies]

Sorry, I'm guessing the statement because my phone isn't displaying any unicode.

[Adam Topaz]

Yeah that’s what I’m wondering too

[Bolton Bailey]

Hmm, seems to me that the proof should work for tsum too. If I take a to be my non-1 element of H, then the point is that tsum H = tsum a H = a tsum H, so either the tsum is zero or we reach a contradiction.

[Adam Topaz]

Slick!

[Bolton Bailey]

I guess separation is needed - docs#tsum_image requires [t2_space α]

[Notification Bot]

Bolton Bailey has marked this topic as resolved.

[Notification Bot]

Bolton Bailey has marked this topic as unresolved.

[Bolton Bailey]

Adam Topaz said:

Do we know that finite subgroups of multiplicative groups of fields are cyclic? I don’t recall seeing such statements in mathlib

Seems we have docs#is_cyclic_of_subgroup_is_domain. Does anyone know how do I get the mul_hom from a subgroup of the units of a field into the field?

[Yakov Pechersky]

docs#units.coe_hom

[Yakov Pechersky]

Note, units is not defined as a subgroup of a monoid, so there's a separate definition instead of docs#subgroup.subtype

[Yakov Pechersky]

Or something similar, the .subtype is too restricted here, it's not for monoids with zero. If it was a subgroup, you'd use docs#submonoid.subtype instead I think (?)

[Eric Wieser]

Compose the subgroup one with the coe one