sum_hom_units_eq_zero
theorem sum_hom_units_eq_zero :
∀ {R : Type u_1} {G : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G] [inst_3 : Fintype G]
(f : G →* R), f ≠ 1 → (Finset.univ.sum fun g => f g) = 0
This theorem states that in an integral domain, if you have a non-trivial homomorphism from a finite group to the integral domain, then the sum of the homomorphic images of all elements of the group is zero.
More formally, for any commutative ring `R` that is an integral domain, any group `G` that is finite, and any group homomorphism `f` from `G` to `R` that is not the identity, the sum of `f(g)` for each `g` in `G` equals zero. This sum is computed over the entire set of elements in `G`, represented by `Finset.univ`.
More concisely: In an integral domain, the sum of the images of a non-identity group homomorphism from a finite group is zero.
|
sum_hom_units
theorem sum_hom_units :
∀ {R : Type u_1} {G : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G] [inst_3 : Fintype G]
(f : G →* R) [inst_4 : Decidable (f = 1)],
(Finset.univ.sum fun g => f g) = ↑(if f = 1 then Fintype.card G else 0)
This theorem states that in an integral domain, which is a commutative ring without zero divisors, the sum of elements which are mapped from a finite group by a homomorphism is zero, unless that homomorphism is the identity function. In that special case, the sum is equal to the cardinality (i.e., the number of elements) of the group.
More concisely: In an integral domain, the sum of images of distinct elements under a homomorphism maps a finite group to zero unless the homomorphism is the identity function, in which case the sum equals the group's cardinality.
|
isCyclic_of_subgroup_isDomain
theorem isCyclic_of_subgroup_isDomain :
∀ {R : Type u_1} {G : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Group G] [inst_3 : Finite G]
(f : G →* R), Function.Injective ⇑f → IsCyclic G
The theorem `isCyclic_of_subgroup_isDomain` states that for any types `R` and `G`, with `R` being a commutative ring and `G` being a finite group, if there exists an injective function `f` from `G` to `R` where `R` is an integral domain, then the group `G` is cyclic. In other words, a finite subgroup of the unit group of an integral domain is always cyclic.
More concisely: If a finite subgroup of the multiplicative group of an integral domain is injectively mapped to the domain, then the group is cyclic.
|