Mathlib.Algebra.Group.Subgroup.Finite

Subgroup.instFintypeSubtypeMemOfDecidablePred instance

(K : Subgroup G) [DecidablePred (· ∈ K)] [Fintype G] : Fintype K

Full source

@[to_additive]
instance (K : Subgroup G) [DecidablePred (· ∈ K)] [Fintype G] : Fintype K :=
  show Fintype { g : G // g ∈ K } from inferInstance

Finite Subgroups of Finite Groups

Informal description

For any subgroup $K$ of a finite group $G$ with a decidable membership predicate, the subgroup $K$ is also finite.

Subgroup.instFiniteSubtypeMem instance

(K : Subgroup G) [Finite G] : Finite K

Full source

@[to_additive]
instance (K : Subgroup G) [Finite G] : Finite K :=
  Subtype.finite

Subgroups of Finite Groups are Finite

Informal description

For any subgroup $K$ of a finite group $G$, the subgroup $K$ is also finite.

Subgroup.list_prod_mem theorem

{l : List G} : (∀ x ∈ l, x ∈ K) → l.prod ∈ K

Full source

/-- Product of a list of elements in a subgroup is in the subgroup. -/
@[to_additive "Sum of a list of elements in an `AddSubgroup` is in the `AddSubgroup`."]
protected theorem list_prod_mem {l : List G} : (∀ x ∈ l, x ∈ K) → l.prod ∈ K :=
  list_prod_mem

Product of Subgroup Elements in a List Belongs to Subgroup

Informal description

Let $G$ be a group and $K$ a subgroup of $G$. For any list $l$ of elements in $G$, if every element $x \in l$ belongs to $K$, then the product of all elements in $l$ (computed in $G$) also belongs to $K$.

Subgroup.multiset_prod_mem theorem

{G} [CommGroup G] (K : Subgroup G) (g : Multiset G) : (∀ a ∈ g, a ∈ K) → g.prod ∈ K

Full source

/-- Product of a multiset of elements in a subgroup of a `CommGroup` is in the subgroup. -/
@[to_additive "Sum of a multiset of elements in an `AddSubgroup` of an `AddCommGroup` is in
 the `AddSubgroup`."]
protected theorem multiset_prod_mem {G} [CommGroup G] (K : Subgroup G) (g : Multiset G) :
    (∀ a ∈ g, a ∈ K) → g.prod ∈ K :=
  multiset_prod_mem g

Product of Multiset in Subgroup is in Subgroup

Informal description

Let $G$ be a commutative group and $K$ a subgroup of $G$. For any multiset $g$ of elements in $G$, if every element $a \in g$ belongs to $K$, then the product of all elements in $g$ (computed in $G$) also belongs to $K$.

Subgroup.multiset_noncommProd_mem theorem

(K : Subgroup G) (g : Multiset G) (comm) : (∀ a ∈ g, a ∈ K) → g.noncommProd comm ∈ K

Full source

@[to_additive]
theorem multiset_noncommProd_mem (K : Subgroup G) (g : Multiset G) (comm) :
    (∀ a ∈ g, a ∈ K) → g.noncommProd comm ∈ K :=
  K.toSubmonoid.multiset_noncommProd_mem g comm

Noncommutative Product of Commuting Multiset Elements in Subgroup Belongs to Subgroup

Informal description

Let $G$ be a group and $K$ a subgroup of $G$. For any multiset $g$ of elements in $G$ where all elements pairwise commute, if every element $a \in g$ belongs to $K$, then the noncommutative product of $g$ (computed in $G$) also belongs to $K$.

Subgroup.prod_mem theorem

 {G : Type*} [CommGroup G] (K : Subgroup G) {ι : Type*} {t : Finset ι} {f : ι → G} (h : ∀ c ∈ t, f c ∈ K) :
  (∏ c ∈ t, f c) ∈ K

Full source

/-- Product of elements of a subgroup of a `CommGroup` indexed by a `Finset` is in the
    subgroup. -/
@[to_additive "Sum of elements in an `AddSubgroup` of an `AddCommGroup` indexed by a `Finset`
 is in the `AddSubgroup`."]
protected theorem prod_mem {G : Type*} [CommGroup G] (K : Subgroup G) {ι : Type*} {t : Finset ι}
    {f : ι → G} (h : ∀ c ∈ t, f c ∈ K) : (∏ c ∈ t, f c) ∈ K :=
  prod_mem h

Product of Subgroup Elements over a Finite Set Belongs to Subgroup

Informal description

Let $G$ be a commutative group and $K$ a subgroup of $G$. For any finite index set $t$ and function $f : \iota \to G$, if $f(c) \in K$ for every $c \in t$, then the product $\prod_{c \in t} f(c)$ belongs to $K$.

Subgroup.noncommProd_mem theorem

 (K : Subgroup G) {ι : Type*} {t : Finset ι} {f : ι → G} (comm) : (∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K

Full source

@[to_additive]
theorem noncommProd_mem (K : Subgroup G) {ι : Type*} {t : Finset ι} {f : ι → G} (comm) :
    (∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K :=
  K.toSubmonoid.noncommProd_mem t f comm

Noncommutative Product of Pairwise Commuting Elements in Subgroup Belongs to Subgroup

Informal description

Let $G$ be a group and $K$ a subgroup of $G$. For any finite index set $\iota$, finite subset $t \subseteq \iota$, and function $f \colon \iota \to G$, if the elements $\{f(c) \mid c \in t\}$ pairwise commute and $f(c) \in K$ for all $c \in t$, then the noncommutative product $\prod_{c \in t} f(c)$ belongs to $K$.

Subgroup.val_list_prod theorem

(l : List H) : (l.prod : G) = (l.map Subtype.val).prod

Full source

@[to_additive (attr := simp 1100, norm_cast)]
theorem val_list_prod (l : List H) : (l.prod : G) = (l.map Subtype.val).prod :=
  SubmonoidClass.coe_list_prod l

Subgroup List Product Coercion Equality: $(l.\text{prod} : G) = (l.\text{map} \ \text{Subtype.val}).\text{prod}$

Informal description

For any subgroup $H$ of a group $G$ and any list $l$ of elements in $H$, the product of $l$ in $H$ (when viewed as an element of $G$) equals the product in $G$ of the elements of $l$ (when each element is viewed as an element of $G$).

Subgroup.val_multiset_prod theorem

{G} [CommGroup G] (H : Subgroup G) (m : Multiset H) : (m.prod : G) = (m.map Subtype.val).prod

Full source

@[to_additive (attr := simp 1100, norm_cast)]
theorem val_multiset_prod {G} [CommGroup G] (H : Subgroup G) (m : Multiset H) :
    (m.prod : G) = (m.map Subtype.val).prod :=
  SubmonoidClass.coe_multiset_prod m

Subgroup Multiset Product Coincides with Group Product in Commutative Groups

Informal description

Let $G$ be a commutative group and $H$ a subgroup of $G$. For any multiset $m$ of elements in $H$, the product of $m$ in $H$ (when viewed as an element of $G$) equals the product in $G$ of the elements of $m$ (when each element is viewed as an element of $G$). In symbols: $$ \left(\prod m\right)_G = \prod_{h \in m} (h)_G $$ where $(\cdot)_G$ denotes the coercion from $H$ to $G$.

Subgroup.val_finset_prod theorem

{ι G} [CommGroup G] (H : Subgroup G) (f : ι → H) (s : Finset ι) : ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : G)

Full source

@[to_additive (attr := simp 1100, norm_cast)]
theorem val_finset_prod {ι G} [CommGroup G] (H : Subgroup G) (f : ι → H) (s : Finset ι) :
    ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : G) :=
  SubmonoidClass.coe_finset_prod f s

Coercion of Finite Product in Subgroup Equals Product in Group

Informal description

Let $G$ be a commutative group and $H$ a subgroup of $G$. For any finite set $s$ indexed by $\iota$ and any function $f \colon \iota \to H$, the product $\prod_{i \in s} f i$ computed in $H$ (when coerced to $G$) equals the product $\prod_{i \in s} f i$ computed directly in $G$.

Subgroup.fintypeBot instance

: Fintype (⊥ : Subgroup G)

Full source

@[to_additive]
instance fintypeBot : Fintype (⊥ : Subgroup G) :=
  ⟨{1}, by
    rintro ⟨x, ⟨hx⟩⟩
    exact Finset.mem_singleton_self _⟩

Finite Type Structure on Trivial Subgroup

Informal description

The trivial subgroup $\bot$ of any group $G$ has a finite type structure.

Subgroup.card_bot theorem

: Nat.card (⊥ : Subgroup G) = 1

Full source

@[to_additive]
theorem card_bot : Nat.card (⊥ : Subgroup G) = 1 := by simp

Cardinality of Trivial Subgroup is One

Informal description

The cardinality of the trivial subgroup $\bot$ of a group $G$ is equal to $1$.

Subgroup.card_top theorem

: Nat.card (⊤ : Subgroup G) = Nat.card G

Full source

@[to_additive]
theorem card_top : Nat.card (⊤ : Subgroup G) = Nat.card G :=
  Nat.card_congr Subgroup.topEquiv.toEquiv

Cardinality of the Top Subgroup Equals Cardinality of the Group

Informal description

For any group $G$, the cardinality of the top subgroup (i.e., $G$ itself) is equal to the cardinality of $G$ as a type. In other words, $\mathrm{card}(\top \text{ subgroup of } G) = \mathrm{card}(G)$.

Subgroup.card_eq_iff_eq_top theorem

[Finite H] : Nat.card H = Nat.card G ↔ H = ⊤

Full source

@[to_additive (attr := simp)]
theorem card_eq_iff_eq_top [Finite H] : Nat.cardNat.card H = Nat.card G ↔ H = ⊤ :=
  Iff.intro (eq_top_of_card_eq H) (fun h ↦ by simpa only [h] using card_top)

Subgroup Cardinality Equals Group Cardinality iff Trivial Subgroup

Informal description

For a finite subgroup $H$ of a group $G$, the cardinality of $H$ equals the cardinality of $G$ if and only if $H$ is the entire group $G$ (i.e., $H = \top$). In other words, $\mathrm{card}(H) = \mathrm{card}(G) \leftrightarrow H = G$.

Subgroup.card_le_one_iff_eq_bot theorem

[Finite H] : Nat.card H ≤ 1 ↔ H = ⊥

Full source

@[to_additive card_le_one_iff_eq_bot]
theorem card_le_one_iff_eq_bot [Finite H] : Nat.cardNat.card H ≤ 1 ↔ H = ⊥ :=
  ⟨H.eq_bot_of_card_le, fun h => by simp [h]⟩

Cardinality Criterion for Trivial Subgroup: $|H| \leq 1 \leftrightarrow H = \{\bot\}$

Informal description

For a finite subgroup $H$ of a group, the cardinality of $H$ is less than or equal to $1$ if and only if $H$ is the trivial subgroup $\{\bot\}$.

Subgroup.one_lt_card_iff_ne_bot theorem

[Finite H] : 1 < Nat.card H ↔ H ≠ ⊥

Full source

@[to_additive one_lt_card_iff_ne_bot]
theorem one_lt_card_iff_ne_bot [Finite H] : 1 < Nat.card H ↔ H ≠ ⊥ :=
  lt_iff_not_le.trans H.card_le_one_iff_eq_bot.not

Cardinality Criterion for Nontrivial Subgroup: $|H| > 1 \leftrightarrow H \neq \{\bot\}$

Informal description

For a finite subgroup $H$ of a group, the cardinality of $H$ is greater than $1$ if and only if $H$ is not the trivial subgroup $\{\bot\}$.

Subgroup.card_le_card_group theorem

[Finite G] : Nat.card H ≤ Nat.card G

Full source

@[to_additive]
theorem card_le_card_group [Finite G] : Nat.card H ≤ Nat.card G :=
  Nat.card_le_card_of_injective _ Subtype.coe_injective

Subgroup Cardinality Bound: $|H| \leq |G|$ for finite groups

Informal description

For any finite group $G$ and any subgroup $H$ of $G$, the cardinality of $H$ is less than or equal to the cardinality of $G$, i.e., $|H| \leq |G|$.

Subgroup.card_le_of_le theorem

{H K : Subgroup G} [Finite K] (h : H ≤ K) : Nat.card H ≤ Nat.card K

Full source

@[to_additive]
theorem card_le_of_le {H K : Subgroup G} [Finite K] (h : H ≤ K) : Nat.card H ≤ Nat.card K :=
  Nat.card_le_card_of_injective _ (Subgroup.inclusion_injective h)

Subgroup Cardinality Inequality: $H \leq K \Rightarrow |H| \leq |K|$ for finite $K$

Informal description

Let $G$ be a group with subgroups $H$ and $K$ such that $H \leq K$ and $K$ is finite. Then the cardinality of $H$ is less than or equal to the cardinality of $K$, i.e., $|H| \leq |K|$.

Subgroup.card_map_of_injective theorem

{H : Type*} [Group H] {K : Subgroup G} {f : G →* H} (hf : Function.Injective f) : Nat.card (map f K) = Nat.card K

Full source

@[to_additive]
theorem card_map_of_injective {H : Type*} [Group H] {K : Subgroup G} {f : G →* H}
    (hf : Function.Injective f) :
    Nat.card (map f K) = Nat.card K := by
  apply Nat.card_image_of_injective hf

Cardinality Preservation of Subgroups under Injective Homomorphisms: $|f(K)| = |K|$

Informal description

Let $G$ and $H$ be groups, $K$ a subgroup of $G$, and $f \colon G \to H$ an injective group homomorphism. Then the cardinality of the image subgroup $f(K)$ equals the cardinality of $K$, i.e., $|f(K)| = |K|$.

Subgroup.card_subtype theorem

(K : Subgroup G) (L : Subgroup K) : Nat.card (map K.subtype L) = Nat.card L

Full source

@[to_additive]
theorem card_subtype (K : Subgroup G) (L : Subgroup K) :
    Nat.card (map K.subtype L) = Nat.card L :=
  card_map_of_injective K.subtype_injective

Cardinality Preservation under Subgroup Inclusion: $|L| = |\text{incl}(L)|$

Informal description

For any subgroup $K$ of a group $G$ and any subgroup $L$ of $K$, the cardinality of the image of $L$ under the inclusion homomorphism $K \to G$ equals the cardinality of $L$, i.e., $|\text{map}(K.\text{subtype})(L)| = |L|$.

Subgroup.pi_mem_of_mulSingle_mem_aux theorem

 [DecidableEq η] (I : Finset η) {H : Subgroup (∀ i, f i)} (x : ∀ i, f i) (h1 : ∀ i, i ∉ I → x i = 1)
  (h2 : ∀ i, i ∈ I → Pi.mulSingle i (x i) ∈ H) : x ∈ H

Full source

@[to_additive]
theorem pi_mem_of_mulSingle_mem_aux [DecidableEq η] (I : Finset η) {H : Subgroup (∀ i, f i)}
    (x : ∀ i, f i) (h1 : ∀ i, i ∉ I → x i = 1) (h2 : ∀ i, i ∈ I → Pi.mulSinglePi.mulSingle i (x i) ∈ H) :
    x ∈ H := by
  induction I using Finset.induction_on generalizing x with
  | empty =>
    have : x = 1 := by
      ext i
      exact h1 i (Finset.not_mem_empty i)
    rw [this]
    exact one_mem H
  | insert i I hnmem ih =>
    have : x = Function.update x i 1 * Pi.mulSingle i (x i) := by
      ext j
      by_cases heq : j = i
      · subst heq
        simp
      · simp [heq]
    rw [this]
    clear this
    apply mul_mem
    · apply ih <;> clear ih
      · intro j hj
        by_cases heq : j = i
        · subst heq
          simp
        · simpa [heq] using h1 j (by simpa [heq] using hj)
      · intro j hj
        have : j ≠ i := by
          rintro rfl
          contradiction
        simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
        exact h2 _ (Finset.mem_insert_of_mem hj)
    · apply h2
      simp

Membership in Product Subgroup via Single-Element Projections

Informal description

Let $\eta$ be a type with decidable equality, $I$ a finite subset of $\eta$, and $H$ a subgroup of the product group $\prod_{i \in \eta} f_i$ where each $f_i$ is a group. For any element $x \in \prod_{i \in \eta} f_i$ such that: 1. $x_i = 1$ for all $i \notin I$, and 2. For each $i \in I$, the function $\text{mulSingle}_i(x_i)$ (which equals $x_i$ at $i$ and $1$ elsewhere) is in $H$, then $x$ itself is in $H$.

Subgroup.pi_mem_of_mulSingle_mem theorem

 [Finite η] [DecidableEq η] {H : Subgroup (∀ i, f i)} (x : ∀ i, f i) (h : ∀ i, Pi.mulSingle i (x i) ∈ H) : x ∈ H

Full source

@[to_additive]
theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : Subgroup (∀ i, f i)} (x : ∀ i, f i)
    (h : ∀ i, Pi.mulSinglePi.mulSingle i (x i) ∈ H) : x ∈ H := by
  cases nonempty_fintype η
  exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i

Membership in Product Subgroup via Single-Element Projections

Informal description

Let $\eta$ be a finite type with decidable equality, and let $H$ be a subgroup of the product group $\prod_{i \in \eta} f_i$, where each $f_i$ is a group. For any element $x \in \prod_{i \in \eta} f_i$, if for every index $i \in \eta$, the function $\text{mulSingle}_i(x_i)$ (which equals $x_i$ at $i$ and $1$ elsewhere) is in $H$, then $x$ itself is in $H$.

Subgroup.pi_le_iff theorem

 [DecidableEq η] [Finite η] {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
  pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J

Full source

/-- For finite index types, the `Subgroup.pi` is generated by the embeddings of the groups. -/
@[to_additive "For finite index types, the `Subgroup.pi` is generated by the embeddings of the
 additive groups."]
theorem pi_le_iff [DecidableEq η] [Finite η] {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
    pipi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J := by
  constructor
  · rintro h i _ ⟨x, hx, rfl⟩
    apply h
    simpa using hx
  · exact fun h x hx => pi_mem_of_mulSingle_mem x fun i => h i (mem_map_of_mem _ (hx i trivial))

Product Subgroup Containment Criterion via Single-Element Embeddings

Informal description

Let $\eta$ be a finite type with decidable equality, and let $(f_i)_{i \in \eta}$ be a family of groups. For any family of subgroups $(H_i)_{i \in \eta}$ where each $H_i$ is a subgroup of $f_i$, and any subgroup $J$ of the product group $\prod_{i \in \eta} f_i$, the following are equivalent: 1. The product subgroup $\prod_{i \in \eta} H_i$ is contained in $J$. 2. For every index $i \in \eta$, the image of $H_i$ under the monoid homomorphism $\text{mulSingle}_i$ (which maps $x \in H_i$ to the function that is $x$ at $i$ and $1$ elsewhere) is contained in $J$.

Subgroup.mem_normalizer_fintype theorem

{S : Set G} [Finite S] {x : G} (h : ∀ n, n ∈ S → x * n * x⁻¹ ∈ S) : x ∈ Subgroup.setNormalizer S

Full source

theorem mem_normalizer_fintype {S : Set G} [Finite S] {x : G} (h : ∀ n, n ∈ S → x * n * x⁻¹ ∈ S) :
    x ∈ Subgroup.setNormalizer S := by
  haveI := Classical.propDecidable; cases nonempty_fintype S
  haveI := Set.fintypeImage S fun n => x * n * x⁻¹
  exact fun n =>
    ⟨h n, fun h₁ =>
      have heq : (fun n => x * n * x⁻¹) '' S = S :=
        Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
          (by rw [Set.card_image_of_injective S conj_injective])
      have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
      let ⟨y, hy⟩ := this
      conj_injective hy.2 ▸ hy.1⟩

Finite Subset Normalizer Membership Criterion

Informal description

Let $G$ be a group and $S$ a finite subset of $G$. If an element $x \in G$ satisfies that for every $n \in S$, the conjugate $x n x^{-1}$ is also in $S$, then $x$ belongs to the normalizer subgroup of $S$ in $G$.

MonoidHom.decidableMemRange instance

(f : G →* N) [Fintype G] [DecidableEq N] : DecidablePred (· ∈ f.range)

Full source

@[to_additive]
instance decidableMemRange (f : G →* N) [Fintype G] [DecidableEq N] : DecidablePred (· ∈ f.range) :=
  fun _ => Fintype.decidableExistsFintype

Decidability of Membership in the Range of a Group Homomorphism

Informal description

For any group homomorphism $f \colon G \to N$ between groups $G$ and $N$, where $G$ is finite and equality is decidable in $N$, the predicate "being in the range of $f$" is decidable. That is, for any $y \in N$, we can algorithmically determine whether there exists $x \in G$ such that $f(x) = y$.

MonoidHom.fintypeMrange instance

{M N : Type*} [Monoid M] [Monoid N] [Fintype M] [DecidableEq N] (f : M →* N) : Fintype (mrange f)

Full source

/-- The range of a finite monoid under a monoid homomorphism is finite.
Note: this instance can form a diamond with `Subtype.fintype` in the
presence of `Fintype N`. -/
@[to_additive "The range of a finite additive monoid under an additive monoid homomorphism is
 finite.

Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the presence
of `Fintype N`."]
instance fintypeMrange {M N : Type*} [Monoid M] [Monoid N] [Fintype M] [DecidableEq N]
    (f : M →* N) : Fintype (mrange f) :=
  Set.fintypeRange f

Finiteness of the Range of a Monoid Homomorphism from a Finite Monoid

Informal description

For any finite monoid $M$, monoid $N$ with decidable equality, and monoid homomorphism $f \colon M \to N$, the range of $f$ is finite.

MonoidHom.fintypeRange instance

[Fintype G] [DecidableEq N] (f : G →* N) : Fintype (range f)

Full source

/-- The range of a finite group under a group homomorphism is finite.

Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the
presence of `Fintype N`. -/
@[to_additive "The range of a finite additive group under an additive group homomorphism is finite.

Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the
 presence of `Fintype N`."]
instance fintypeRange [Fintype G] [DecidableEq N] (f : G →* N) : Fintype (range f) :=
  Set.fintypeRange f

Finiteness of the Range of a Group Homomorphism from a Finite Group

Informal description

For any finite group $G$, group $N$ with decidable equality, and group homomorphism $f \colon G \to N$, the range of $f$ is finite.

Fintype.card_coeSort_mrange theorem

 {M N : Type*} [Monoid M] [Monoid N] [Fintype M] [DecidableEq N] {f : M →* N} (hf : Function.Injective f) :
  Fintype.card (mrange f) = Fintype.card M

Full source

lemma _root_.Fintype.card_coeSort_mrange {M N : Type*} [Monoid M] [Monoid N] [Fintype M]
    [DecidableEq N] {f : M →* N} (hf : Function.Injective f) :
    Fintype.card (mrange f) = Fintype.card M :=
  Set.card_range_of_injective hf

Cardinality of Range of Injective Monoid Homomorphism Equals Domain Cardinality

Informal description

Let $M$ and $N$ be monoids with $M$ finite and $N$ having decidable equality. For any injective monoid homomorphism $f \colon M \to N$, the cardinality of the range of $f$ (as a submonoid of $N$) equals the cardinality of $M$, i.e., $$|\mathrm{mrange}\, f| = |M|.$$

Fintype.card_coeSort_range theorem

[Fintype G] [DecidableEq N] {f : G →* N} (hf : Function.Injective f) : Fintype.card (range f) = Fintype.card G

Full source

lemma _root_.Fintype.card_coeSort_range [Fintype G] [DecidableEq N] {f : G →* N}
    (hf : Function.Injective f) :
    Fintype.card (range f) = Fintype.card G :=
  Set.card_range_of_injective hf

Cardinality of Range of Injective Group Homomorphism Equals Domain Cardinality

Informal description

Let $G$ be a finite group and $N$ a group with decidable equality. For any injective group homomorphism $f \colon G \to N$, the cardinality of the range of $f$ is equal to the cardinality of $G$, i.e., $$|\mathrm{range}\, f| = |G|.$$

Tags