lean-bench pilot: label 65 items

Definition 1.11.8. A field is a commutative ring with multiplicative identity element $1 \neq 0$ in which every nonzero element is a unit.

class Field (F : Type*) extends CommRing F, Nontrivial F where \\(nonzero_is_unit : ∀ (a : F), a ≠ 0 → IsUnit a)

Example 2.2.3. In any group $G$, $G$ itself and $\{e\}$ are subgroups.

theorem group_and_trivial_subgroups (G : Type*) [Group G] : Subgroup G (Set.univ : Set G) ∧ Subgroup G {1} := by sorry

1.11.1. Show that the only units in the ring of integers are $\pm 1$.

theorem units_in_integers_are_pm_one : (u : ℤ) → IsUnit u → u = 1 ∨ u = -1 := by sorry

Let $a$ be an element of a group $G$. The subgroup $\langle a \rangle$ generated by $a$ is $\{a^k : k \in \mathbb{Z}\}$.
\end{proposition}

\begin{proof}
The formulas $a^k a^l = a^{k+l}$ and $(a^k)^{-1} = a^{-k}$ show that $\{a^k : k \in \mathbb{Z}\}$ is a subgroup of $G$ containing $a = a^1$. Therefore, $\langle a \rangle \subseteq \{a^k : k \in \mathbb{Z}\}$. On the other hand, a subgroup is always is closed under taking integer powers, so $\langle a \rangle \supseteq \{a^k : k \in \mathbb{Z}\}$.

theorem subgroup_generated_by_element {G : Type*} [Group G] (a : G) : \<a\> = {a ^ k | k : ℤ} := by \\(sorry)

Definition 2.1.13. We say that two groups $G$ and $H$ are isomorphic if there is a bijection $\varphi : G \longrightarrow H$ such that for all $g_1, g_2 \in G$ $\varphi(g_1g_2) = \varphi(g_1)\varphi(g_2)$. The map $\varphi$ is called an isomorphism.

def isIsomorphicGroups (G H : Type*) [Group G] [Group H] : Prop :=">"> ∃ φ : G → H, Function.Bijective φ ∧ ∀ g₁ g₂ : G, φ (g₁ * g₂) = φ g₁ * φ g₂

Proposition 2.1.4. Let $G$ be a group and let $a, b \in G$. Then $(ab)^{-1} = b^{-1}a^{-1}$

Proof. It suffices to show that $(ab)(b^{-1}a^{-1}) = e$. But by associativity, $(ab)(b^{-1}a^{-1}) = a(b(b^{-1}a^{-1})) = a((bb^{-1})a^{-1}) = a(ea^{-1}) = aa^{-1} = e$.

theorem inverse_of_product_in_group {G : Type*} [Group G] (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by \\[1em]  have h : (a * b) * (b⁻¹ * a⁻¹) = 1 := by \\[1em]    calc (a * b) * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) := by simp only [mul_assoc] \\[1em]    _ = a * ((b * b⁻¹) * a⁻¹) := by simp only [mul_assoc] \\[1em]    _ = a * (1 * a⁻¹) := by simp only [mul_left_inv, one_mul] \\[1em]    _ = a * a⁻¹ := by simp only [one_mul] \\[1em]    _ = 1 := by simp only [mul_left_inv] \\[1em]  exact mul_left_cancel₀ h

1.12.2. Show that if a snoop were able to find $\varphi(n)$, then he could also find $p$ and $q$.

theorem snoop_finding_totient_implies_finding_factors (n p q : ℕ) (hn : n = p * q) (hpq : p.Prime ∧ q.Prime) : ∃ (φ : ℕ → ℕ), (∀ m, φ m = Nat.totient m) → ∃ (p' q' : ℕ), n = p' * q' ∧ p'.Prime ∧ q'.Prime := by sorry

Proposition 2.1.18. If $\varphi : G \to H$ is an isomorphism, then $\varphi(e_G) = e_H$, and for each $g \in G$, $\varphi(g^{-1}) = \varphi(g)^{-1}$.

Proof. For any $h \in H$, there is a $g \in G$ such that $\varphi(g) = h$. Then
$\varphi(e_G)h = \varphi(e_G)\varphi(g) = \varphi(e_G g) = \varphi(g) = h$. Hence by the uniqueness
of the identity in $H$, $\varphi(e_G) = e_H$. Likewise, $\varphi(g^{-1})\varphi(g) = \varphi(gg^{-1}) = \varphi(e_G) = e_H$. This shows that $\varphi(g^{-1}) = \varphi(g)^{-1}$.

theorem isomorphism_preserves_identity_and_inverses {G H : Type*} [Group G] [Group H] (φ : G ≃* H) : φ (1 : G) = (1 : H) ∧ ∀ g : G, φ g⁻¹ = (φ g)⁻¹ := by\n  have h_id : φ (1 : G) = (1 : H) := by\n    intro h,\n    obtain ⟨g, hg⟩ := φ.surjective h,\n    calc\n      φ (1 : G) * h = φ (1 : G) * φ g := by rw [hg]\n      _ = φ (1 : G * g) := by simp [φ.map_mul]\n      _ = φ g := by simp [one_mul]\n      _ = h := by rw [hg],\n    exact mul_left_cancel₀ h_id (φ (1 : G)),\n  have h_inv : ∀ g : G, φ g⁻¹ = (φ g)⁻¹ := by\n    intro g,\n    calc\n      φ g⁻¹ * φ g = φ (g⁻¹ * g) := by simp [φ.map_mul]\n      _ = φ (1 : G) := by simp [mul_inv_cancel]\n      _ = (1 : H) := by rw [h_id],\n    exact mul_left_cancel₀ (φ g⁻¹ * φ g) (1 : H),\n  exact ⟨h_id, h_inv⟩

2.1.5. Show that the groups $\mathbb{Z}_4$ and the group of rotational symmetries of
the rectangle are not isomorphic, although each group has four elements.
Hint: In one of the groups, but not the other, each element has square equal
to the identity. Show that if two groups $G$ and $H$ are isomorphic, and $G$
has the property that each element has square equal to the identity, then $H$
also has this property.

2.1.6. Suppose that $\varphi : G \to H$ is an isomorphism of groups. Show that
for all $g \in G$ and $n \in \mathbb{N}$, $\varphi(g^n) = (\varphi(g))^n$. Show that if $g^n = e$, then
also $(\varphi(g))^n = e$.

theorem zmod_four_not_isomorphic_to_rectangle_rotational_symmetries : ¬ (ZMod 4) ≃* (DihedralGroup 2) := by sorry

Corollary 2.1.6. Let $G$ be a group and let $a$ and $b$ be elements of $G$. The equation $ax = b$ has a unique solution $x$ in $G$, and likewise the equation $xa = b$ has a unique solution in $G$.

theorem unique_solution_to_group_equation {G : Type*} [Group G] (a b : G) : \\(∃! x : G, a * x = b) ∧ (∃! x : G, x * a = b) := by\n  sorry

If $G$ is a finite group of size $n$, then for every element $g \in G$, we have $g^n = e$.

theorem finite_group_element_power_equals_identity (G : Type*) [Group G] [Fintype G] (g : G) : g ^ Fintype.card G = 1 := by sorry

1.12.4. How can André and Bernice adapt the RSA method so that they
can exchange messages that are both secure and authenticated?

theorem adapt_rsa_for_secure_and_authenticated_messages : \u2203 (adaptation : Type), \u2200 (message : Type) (encrypt decrypt : message \u2192 message), secure (encrypt \u2218 decrypt) \u21d2 authenticated (encrypt \u2218 decrypt) := by sorry

Since $\Phi(n)$ is a group of size $|\Phi(n)| = \varphi(n)$, we have $[a]^{\varphi(n)} = [1]$, for all $[a] \in \Phi(n)$, by the theorem of group theory just mentioned. But $[a] \in \Phi(n)$ if, and only if, $a$ is relatively prime to $n$, and $[a]^{\varphi(n)} = [1]$ translates to $a^{\varphi(n)} \equiv 1 \mod n$.

theorem euler_totient_theorem (n : ℕ) (a : ℤ) (h : Nat.Coprime a n) : (a ^ Nat.totient n) ≡ 1 [ZMOD n] := by sorry

(a) Let $X$ be any set. Show that the set of functions from $X$ to $\mathbb{R}$ is a ring. What is the multiplicative identity? What are the units?

theorem functions_from_set_to_real_form_a_ring (X : Type) : Ring (X → ℝ) := by sorry

Corollary 2.1.8. If $G$ is a finite group, each row and each column of the multiplication table of $G$ contains each element of $G$ exactly once.

Proof. You are

theorem finite_group_multiplication_table_rows_and_columns (G : Type*) [Group G] [Fintype G] (g h : G) :\\\n  ∃! (x : G), x * g = h \\\n  ∧ ∃! (y : G), g * y = h := by \\\n  sorry

(a) Let $G \cong H \times K$ be a direct product of finite groups. Show that every element in $G$ has order dividing $\mathrm{l.c.m.}(|H|, |K|)$.

theorem order_divides_lcm_in_direct_product (H K : Type*) [Fintype H] [Fintype K] [Group H] [Group K] (g : H × K) : OrderOf g ∣ lcm (Fintype.card H) (Fintype.card K) := by sorry

Example 1.11.9.
(a) $\mathbb{R}, \mathbb{Q}$, and $\mathbb{C}$ are fields.
(b) $\mathbb{Z}$ is not a field. $\mathbb{R}[x]$ is not a field.

theorem examples_of_fields_and_non_fields : IsField ℝ ∧ IsField ℚ ∧ IsField ℂ ∧ ¬IsField ℤ := by sorry

Example 2.2.4. The set of all complex numbers of modulus (absolute value) equal to 1 is a subgroup of the group of all nonzero complex numbers, with multiplication as the group operation. See Appendix D.

theorem unit_circle_is_subgroup : IsSubgroup (SetOf (fun z : ℂ => ∥z∥ = 1)) (· * ·) := by sorry

Definition 2.2.16. The order of the cyclic subgroup generated by $a$ is called the order of $a$. We denote the order of $a$ by $o(a)$.

def orderOfElement (G : Type*) [Group G] (a : G) : ℕ := Nat.orderOf a

2.1.3. Prove the following refinement of the uniqueness of the identity in
a group: Let $G$ be a group with identity element $e$, and let $e', g \in G$.
Suppose $e'$ and $g$ are elements of $G$. If $e'g = g$, then $e' = e$. (This result
says that if a group element acts like the identity when multiplied by one
element on one side, then it is the identity.)

theorem uniqueness_of_identity_refinement (G : Type*) [Group G] (e' g : G) (h : e' * g = g) : e' = 1 := by sorry

2.1.7. Suppose that $\varphi : G \to H$ is an isomorphism of groups. Show that $G$ is abelian if and only if $H$ is abelian.

theorem isomorphism_preserves_abelian_property {G H : Type*} [Group G] [Group H] (φ : G ≃* H) :\\\n  Commutative (*) ↔ Commutative ((*) : H → H → H) := by sorry

2.1.4. Show that each row and each column of the multiplication table of
a finite group contains each group element exactly once. Use Proposition
2.1.5.

theorem finite_group_multiplication_table_properties (G : Type*) [Fintype G] [Group G] : \/\n  (∀ g : G, ∀ g' : G, ∃! h : G, g * h = g') ∧ \/\n  (∀ g : G, ∀ g' : G, ∃! h : G, h * g = g') := by\n  sorry

(b) Let $n = pq$ be the product of two primes, and let $m = \mathrm{l.c.m.}(p-1, q-1)$. Use the isomorphism $\Phi(pq) \cong \Phi(p) \times \Phi(q)$ to show that $a^m \equiv 1 \mod n$ whenever $a$ is relatively prime to $n$.

theorem exercise_1_12_1_b (p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (n : ℕ) (hn : n = p * q) (m : ℕ) (hm : m = Nat.lcm (p - 1) (q - 1)) (a : ℕ) (ha : Nat.Coprime a n) : a ^ m ≡ 1 [ZMOD n] := by sorry

2.1.2. Consider a square with one pair of opposite vertices painted red and
the other pair of vertices painted blue. Determine the symmetry group of
the painted square. That is, describe all the (color-preserving) symme-
tries, find the size of the group and determine whether it is isomorphic to
a known group of the same size. If it is an entirely new group, determine
its multiplication table.

theorem symmetry_group_of_painted_square : ∃ (G : Type) [Group G] [Fintype G], (∀ (g : G), g ≠ 1 → g * g = 1) ∧ Fintype.card G = 4 := by sorry

Corollary 2.1.7. (Cancellation). Suppose $a, x, y$ are elements of a group $G$. If $ax = ay$, then $x = y$. Similarly, if $xa = ya$, then $x = y$.

Proof. The

theorem group_cancellation_law {G : Type*} [Group G] (a x y : G) : a * x = a * y → x = y := by sorry theorem group_cancellation_law' {G : Type*} [Group G] (a x y : G) : x * a = y * a → x = y := by sorry

Lemma 1.12.1. For all integers $a$ and $h$, if $h \equiv 1 \mod m$, then $a^h \equiv a \mod n$.

Proof. Write $h = tm + 1$. Then $a^h = a a^{tm}$, so $a^h - a = a(a^{tm} - 1)$. We have to show that $a^h - a$ is divisible by $n$.

If $q$ does not divide $a$, then $a$ is relatively prime to $q$, so $a^{q-1} \equiv 1 \mod q$, by Fermat's little theorem, Proposition 1.9.10. Since $(q-1)$ divides $tm$, it follows that $a^{tm} \equiv 1 \mod q$; that is $q$ divides $a^{tm} - 1$. Thus, either $q$ divides $a$, or $q$ divides $a^{tm} - 1$, so $q$ divides $a^h - a = a(a^{tm} - 1)$ in any case.

theorem lemma_1_12_1 (a h m n : ℤ) (hn : h % m = 1) (hm : m ∣ n) : a ^ h ≡ a [ZMOD n] := by \\[1em]  sorry

Example 2.2.6. In the permutation group $S_4$, the set of permutations $\pi$ satisfying $\pi(4) = 4$ is a subgroup. This subgroup, since it permutes the numbers $\{1,2,3\}$ and leaves 4 fixed, is isomorphic to $S_3$.

theorem subgroup_of_S4_isomorphic_to_S3 : IsSubgroup {π : SymmetricGroup 4 | π 4 = 4} ∧ Nonempty (SymmetricGroup 4 ⧸ {π : SymmetricGroup 4 | π 4 = 4} ≃* SymmetricGroup 3) := by \\[1em]  sorry

1.11.11. Show that the set of real numbers of the form $a + b\sqrt{2}$, where $a$ and $b$ are rational is a field. Show that $a + b\sqrt{2} \mapsto a - b\sqrt{2}$ is an isomorphism of this field onto itself.

theorem rational_linear_combination_sqrt_two_is_field_with_isomorphism : \\\\   let F : Set ℝ := { x | ∃ a b : ℚ, x = a + b * (2 : ℝ) ^ (1/2) }, \\\\   IsField F ∧ IsFieldHom (F → F) (fun x => match x with \\\\     | a + b * (2 : ℝ) ^ (1/2) => a - b * (2 : ℝ) ^ (1/2)) := by \\\\   sorry

2.1.6. Suppose that $\varphi : G \to H$ is an isomorphism of groups. Show that
for all $g \in G$ and $n \in \mathbb{N}$, $\varphi(g^n) = (\varphi(g))^n$. Show that if $g^n = e$, then
also $(\varphi(g))^n = e$.

theorem isomorphism_preserves_powers_and_order {G H : Type*} [Group G] [Group H] (φ : G →* H) (hφ : Function.Bijective φ) (g : G) (n : ℕ) :\/\/  φ(g^n) = (φ g)^n ∧ (g^n = 1 → (φ g)^n = 1) := by\n  sorry

2.1.17. Let $M$ be a set with an associative operation and let $N$ be a subset which is closed under the operation. Show that $N$ is also closed for the product of an arbitrary number of elements; i.e., if $n \geq 1$ and $a_1, a_2, \ldots, a_n \in N$, then $a_1 a_2 \cdots a_n \in N$.

theorem subset_closed_under_arbitrary_product {M : Type*} [Semigroup M] (N : Set M) (hN : ∀ x y ∈ N, x * y ∈ N) (n : ℕ) (hn : 1 ≤ n) (a : Fin n → M) (ha : ∀ i, a i ∈ N) : (∏ i, a i) ∈ N :=\sorry

Next, we want to check that the map $\varphi$ is a homomorphism of rings. We leave this to the reader as an exercise, see Exercise 1.11.9.

theorem check_phi_is_ring_homomorphism (R S : Type*) [Ring R] [Ring S] (φ : R → S) : IsRingHom φ := by sorry

(b) Let $T$ be any $n$-by-$n$ matrix with real entries. We can define a ring homomorphism from $\mathbb{R}[x]$ to $\mathrm{Mat}_n(\mathbb{R})$ by

$$
a_0 + a_1x + \cdots + a_sx^s \mapsto a_0 + a_1T + \cdots + a_sT^s.

theorem matrix_ring_homomorphism_from_polynomial (n : ℕ) (T : Matrix n n ℝ) : RingHom (Polynomial ℝ) (Matrix n n ℝ) := by sorry

2.1.10. Show that any group with four elements must have a nonidentity element whose square is the identity. That is, some nonidentity element must be its own inverse.

Hint: If you already knew that there were exactly two groups of order four, up to isomorphism, namely $\mathbb{Z}_4$ and the group of rotational symmetries of the rectangle, then you could verify the statement by checking that these two groups have the desired property. But our purpose is to prove that these are the only two groups of order 4, so we are not allowed to use this information in the proof!

So you must start by assuming that you have a group $G$ with four elements; you may not assume anything else about $G$ except that it is a group and that it has four elements. You must show that one of the three nonidentity elements has square equal to $e$. Call the elements of the group $\{e, a, b, c\}$. There are two possibilities: Each nonidentity element has square equal to $e$, in which case there is nothing more to show, or some element does not have square equal to $e$. Suppose that $a^2 \ne e$. Thus, $a \ne a^{-1}$. Without loss of generality, write $b = a^{-1}$. Then also $a = b^{-1}$. Then what is the inverse of $c$?

theorem group_of_four_has_self_inverse_nonidentity (G : Type) [Group G] (hG : Fintype.card G = 4) : ∃ g : G, g ≠ 1 ∧ g * g = 1 := by sorry

Example 2.1.16. $S_3$ is nonabelian and $\mathbb{Z}_6$ is abelian. Thus these are two nonisomorphic groups of order 6.

theorem s3_nonabelian_z6_abelian : !IsAbelian (Symmetric 3) ∧ IsAbelian (ZMod 6) := by \\[0.5em] sorry

} Let $M$ be a set with an associative operation, $M \times M \longrightarrow M$, denoted by juxtaposition. For every $n \geq 1$, there is a unique product $M^n \longrightarrow M$,
$$
(a_1,a_2,\ldots,a_n) \mapsto a_1a_2\cdots a_n,
$$
such that
\begin{enumerate}
\item[(a)] The product of one element is that element $(a) = a$.
\item[(b)] The product of two elements agrees with the given operation $(ab) = ab$.
\item[(c)] For all $n \geq 2$, for all $a_1,\ldots a_n \in M$, and for all $1 \leq k \leq n-1$,
$$
a_1a_2\cdots a_n = (a_1\cdots a_k)(a_{k+1}\cdots a_n).
$$

theorem unique_associative_product (M : Type*) [Semigroup M] (n : ℕ) (h : n ≥ 1) : ∃! f : (Fin n → M) → M, (∀ a : M, f ![a] = a) ∧ (∀ a b : M, f ![a, b] = a * b) ∧ (∀ (k : ℕ) (hk : 1 ≤ k) (hnk : k < n) (a : Fin n → M), f a = f (a ↾ k) * f (a ∘ (Fin.succAbove k).symm)) := by sorry

(b) $C_n$ is a cyclic group of order $n$ with generator $\xi = e^{2\pi i/n}$.

theorem cyclic_group_of_order_n (n : ℕ) (h : n > 0) : IsCyclic (ZMod n) := by sorry

(a) $C_n = \{e^{2\pi i k/n} : 0 \leq k \leq n-1\}$.

def cyclicGroupOfNthRootsOfUnity (n : ℕ) : Subgroup ℂ :=">",

These conditions also suffice for $H$ to be a subgroup. Associativity of the product is inherited from $G$, so it need not be checked. Also, if conditions (1) and (2) are satisfied, then $e$ is automatically in $H$; indeed, $H$ is nonempty, so contains some element $h$; according to (2), $h^{-1} \in H$ as well, and then according to (1), $e = h h^{-1} \in H$.

theorem subgroup_conditions_suffice {G : Type*} [Group G] (H : Set G) (h_one : ∀ h ∈ H, h⁻¹ ∈ H) (h_mul : ∀ h1 h2 ∈ H, h1 * h2 ∈ H) : IsSubgroup H := by \\- sorry

1.11.3. A Laurent polynomial is a "polynomial" in which negative as well as positive powers of the variable $x$ are allowed, for example, $p(x) = 7x^{-3} + 4x^{-2} + 4 + 2x$. Show that the set of Laurent polynomials with coefficients in a field $K$ forms a ring with identity. This ring is denoted by $K[x, x^{-1}]$. (If you prefer, you may take $K = \mathbb{R}$.) What are the units?

theorem laurent_polynomials_form_ring_with_identity (K : Type*) [Field K] : Ring (LaurentSeries K) := by sorry

Example 1.11.6.

(a) The map $f : \mathbb{Z} \to \mathbb{Z}_n$ defined by $f(a) = [a]$ is a homomorphism of rings, because

$$
f(a + b) = [a + b] = [a] + [b] = f(a) + f(b),
$$

and

$$
f(ab) = [ab] = [a][b] = f(a)f(b)

theorem int_to_zmod_n_is_ring_hom (n : ℕ) : RingHom ℤ (ZMod n) := by \\_refine' { toFun := fun a => (a : ZMod n), \\_ \\_ map_one' := _, \\_ \\_ map_mul' := _, \\_ \\_ map_add' := _ }; \\_ intros; \\_ rfl

Example 2.1.15. For any natural number $n$, the symmetric group $S_n$ is a group of order $n!$. According to Exercise 1.5.8, for all $n \geq 3$, $S_n$ is nonabelian.

theorem symmetric_group_order_and_nonabelian (n : ℕ) (hn : n ≥ 3) :\n  Fintype.card (Symmetric n) = n! ∧ ¬ IsAbelian (Symmetric n) := by\n  sorry

For a nonempty subset $H$ of $G$ to be a subgroup of $G$, it is necessary that
1. For all elements $h_1$ and $h_2$ of $H$, the product $h_1 h_2$ is also an element of $H$.

theorem subset_is_subgroup_condition {G : Type*} [Group G] (H : Set G) (h_nonempty : H.Nonempty) (h_prod : ∀ h1 h2 ∈ H, h1 * h2 ∈ H) : IsSubgroup H := by\nsorry

2.1.8. Show that there is up to isomorphism only one group of order 2.
Hint: Call the elements $\{e, a\}$. Show that there is only one possible multiplication table. Since the row and the column labeled by $e$ are known, there is only one entry of the table that is not known. But that entry is determined by the requirement that each row and column contain each group element.

theorem unique_group_of_order_two_up_to_isomorphism (G H : Type) [Group G] [Group H] [Fintype G] [Fintype H] (hG : Fintype.card G = 2) (hH : Fintype.card H = 2) : Nonempty (G ≃* H) := by sorry

Definition 2.1.14. A group $G$ is called abelian (or commutative) if for all elements $a, b \in G$, the products in the two orders are equal: $ab = ba$.

class IsAbelianGroup (G : Type*) [Group G] : Prop :=">"> (commutative : ∀ a b : G, a * b = b * a)

2.1.9. Show that there is up to isomorphism only one group of order 3.
Hint: Call the elements $\{e, a, b\}$. Show that there is only one possible multiplication table. Since the row and column labeled by $e$ are known, there are four table entries left to determine. Show that there is only one way to fill in these entries that is consistent with the requirement that each row and column contain each group element exactly once.

theorem unique_group_of_order_three_up_to_isomorphism : ∃! (G : Type) [Group G], Fintype G ∧ Fintype.card G = 3 := by sorry

1.11.5. Show that the set of polynomials with real coefficients in three variables, $\mathbb{R}[x, y, z]$ is a ring with identity. What are the units?

theorem polynomials_in_three_variables_form_a_ring_with_identity : Ring (Polynomial (ℝ × ℝ × ℝ)) := by sorry

Thus, $\langle d \rangle = d\mathbb{Z} = \{nd : n \in \mathbb{Z}\}$ is a cyclic subgroup of $\mathbb{Z}$. Note that $\langle d \rangle = \langle -d \rangle$.

theorem cyclic_subgroup_of_int (d : ℤ) : (Submodule.span ℤ {d}) = {n * d | n : ℤ} := by sorry

Proposition 2.1.2. (Uniqueness of inverses). Let $G$ be a group and $h, g \in G$. If $hg = e$, then $h = g^{-1}$.

theorem uniqueness_of_inverses {G : Type*} [Group G] (h g : G) (hg : h * g = 1) : h = g⁻¹ := by sorry

Corollary 2.1.3. Let $g$ be an element of a group $G$. We have $g = (g^{-1})^{-1}$.

Proof. Since $gg^{-1} = e$, it follows from the proposition that $g$ is the inverse of $g^{-1}$.

theorem inverse_of_inverse_is_original_element {G : Type*} [Group G] (g : G) : g = (g⁻¹)⁻¹ := by \\[1ex]\\\\ sorry

A \emph{ring} is a (nonempty) set $R$ with two operations: addition, denoted here by $+$, and multiplication, denoted by juxtaposition, satisfying the following requirements:
\begin{enumerate}
    \item[(a)] Under addition, $R$ is an abelian group.
    \item[(b)] Multiplication is associative.
    \item[(c)] Multiplication distributes over addition: $a(b + c) = ab + ac$, and $(b + c)a = ba + ca$ for all $a,b,c \in R$.
\end{enumerate}

structure Ring (R : Type*) extends AddCommGroup R, Mul R where \\(mul_assoc : ∀ (a b c : R), (a * b) * c = a * (b * c)) \\(left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c) \\(right_distrib : ∀ (a b c : R), (b + c) * a = b * a + c * a)

1.10.2. Show that $C_4 = \{i, -1, -i, 1\}$ is a group under complex multiplication, with 1 the identity element.

theorem cyclic_group_of_fourth_roots_of_unity : IsGroup (Complex.mul) (1 : ℂ) {i, -1, -i, 1} := by sorry

1.11.2. Let $K$ be any field. (If you prefer, you may take $K = \mathbb{R}$.) Show that the set $K[x]$ of polynomials with coefficients in $K$ is a commutative ring with the usual addition and multiplication of polynomials. Show that the constant polynomial 1 is the multiplicative identity, and the only units are the constant polynomials.

theorem polynomial_ring_properties (K : Type*) [Field K] : \\[isCommutativeRing (Polynomial K) ∧ (1 : Polynomial K) = 1 ∧ ∀ p : Polynomial K, IsUnit p → ∃ a : K, p = C a := by \\- sorry

Definition 2.1.10. The order of a group is its size or cardinality. We will denote the order of a group $G$ by $|G|$

def orderOfGroup (G : Type*) [Group G] [Fintype G] : ℕ := Fintype.card G

In $\mathbb{Z}_n$, the cyclic subgroup generated by an element $[d]$ is $\langle [d] \rangle = \{[kd] : k \in \mathbb{Z}\} = \{[k][d] : [k] \in \mathbb{Z}_n\}$.

theorem cyclic_subgroup_in_zmod (n d : ℕ) (hn : 0 < n) :\\\n  (ZMod n).subgroup.closure ({ZMod.mk d} : Set (ZMod n)) = \\\n  {ZMod.mk (k * d % n) | k : ℤ} = \\\n  {ZMod.mk (k * d % n) | k : ZMod n} := by\\\n  sorry

If two groups are isomorphic, then either they are both abelian or both nonabelian. That is, if one of two groups is abelian and the other is nonabelian, then the two groups are not isomorphic (exercise).

theorem isomorphicGroupsHaveSameAbelianProperty (G H : Type*) [Group G] [Group H] (iso : G ≃* H) : (IsAbelian G ↔ IsAbelian H) := by sorry

1.12.3. Suppose that André needs to send a message to Bernice in such a way that Bernice will know that the message comes from André and not from some impostor. The issue here is not the secrecy of the message but rather its authenticity. How can the RSA method be adapted to solve the problem of message authentication?

theorem rsa_message_authentication : ∃ (method : String), method = "Adapted RSA for message authentication" := by sorry

A map $f : R \to S$ between two rings is said to be a homomorphism if it ``respects'' the ring structures. More explicitly, $f$ must take sums to sums and products to products. In notation, $f(a + b) = f(a) + f(b)$ and $f(ab) = f(a)f(b)$ for all $a, b \in R$. A bijective homomorphism is called an isomorphism.

theorem is_ring_hom_iff_respects_operations {R S : Type*} [Ring R] [Ring S] (f : R → S) : Function.IsRingHom f ↔ (∀ a b : R, f (a + b) = f a + f b ∧ f (a * b) = f a * f b) := by\n  sorry

You are asked to show in Exercise 2.1.5 that $\mathbb{Z}_4$ is not isomorphic to the group of rotational symmetries of a rectangular card. Thus there exist at least two nonisomorphic groups of order 4.

theorem zmod_four_not_isomorphic_to_rectangular_card_symmetries : ¬ (ZMod 4) ≃* (DihedralGroup 2) := by sorry

Definition 2.2.1. A nonempty subset $H$ of a group $G$ is called a subgroup if $H$ is itself a group with the group operation inherited from $G$. We write $H \leq G$ to indicate that $H$ is a subgroup of $G$.

theorem is_subgroup_iff_is_group_with_inherited_operation (G : Type*) [Group G] (H : Set G) (h_nonempty : H.Nonempty) : Subgroup.of G H ↔ IsGroup (H, (*), 1, ⁻¹) := by\n  sorry

1.10.7. A $C^1$ diffeomorphism of $\mathbb{R}^3$ is a bijective map $T : \mathbb{R}^3 \to \mathbb{R}^3$ having continuous first-order partial derivatives. Show that the set of $C^1$ diffeomorphisms of $\mathbb{R}^3$ forms a group under composition of maps. (You can replace $\mathbb{R}^3$ with any open subset of $\mathbb{R}^n$.)

theorem C1_diffeomorphisms_form_group (U : Set (ℝ × ℝ × ℝ)) (hU : IsOpen U) :\\\n  Group (Subtype (fun T : (ℝ × ℝ × ℝ) → (ℝ × ℝ × ℝ) => \\\n    Bijective T ∧ DifferentiableOn ℝ T U ∧ ContinuousOn (fun x => deriv (T ∘ (Prod.fst, Prod.snd, Prod.third)) x) U)) := by\\\n  sorry

1.10.6. A homeomorphism of $\mathbb{R}^3$ is a bijective map $T : \mathbb{R}^3 \to \mathbb{R}^3$ such that both $T$ and its inverse are continuous. Show that the set of homeomorphisms of $\mathbb{R}^3$ forms a group under composition of maps. (You can replace $\mathbb{R}^3$ with any metric space or, more generally, with any topological space. Do not confuse the similar words homomorphism and homeomorphism.)

theorem homeomorphisms_form_group : Group (Homeomorph ℝ³ ℝ³) := by sorry

Proposition 2.2.17. If the order of $a$ is finite, then it is the least positive integer $n$ such that $a^n = e$. Furthermore, $\langle a \rangle = \{a^k : 0 \leq k < o(a)\}$.

theorem order_of_element_finite_and_subgroup_generated (G : Type*) [Group G] (a : G) (ha : IsOfFinOrder a) :\/\/ (orderOf a = (min {n : ℕ | n > 0 ∧ a ^ n = 1})) ∧ (Subgroup.closure ({a} : Set G) = {a ^ k | k : ℕ, k < orderOf a}) := by\n  sorry

Proposition 2.1.1. (Uniqueness of the identity). Let $G$ be a group and suppose $e$ and $e'$ are both identity elements in $G$; that is, for all $g \in G$, $eg = ge = e'g = ge' = g$. Then $e = e'$.

theorem uniqueness_of_group_identity {G : Type*} [Group G] (e e' : G) (h_e : ∀ g : G, e * g = g ∧ g * e = g) (h_e' : ∀ g : G, e' * g = g ∧ g * e' = g) : e = e' := by \\[1em]  rw [← h_e' e, h_e e'], \\[1em]  rfl

o $n$.

Lemma 1.12.2. For all integers $a$, if
$$
b \equiv a^r \mod n,
$$
then
$$
b^s \equiv a \mod n.
$$

Proof. Write $rs = 1 + tm$ Then $b^s \equiv a^{rs} \equiv a \mod n$, by Lemma 1.12.1.

theorem lemma_1_12_2 (a b r s n t : ℤ) (h1 : b ≡ a^r [ZMOD n]) (h2 : r * s = 1 + n * t) : b^s ≡ a [ZMOD n] := by sorry

2.1.1. Determine the symmetry group of a nonsquare rhombus. That is, de-
scribe all the symmetries, find the size of the group, and determine whether
it is isomorphic to a known group of the same size. If it is an entirely new
group, determine its multiplication table.

theorem symmetry_group_of_nonsquare_rhombus : ∃ (G : Type) [Group G], Finite G ∧ ∃ (n : ℕ), Fintype.card G = n ∧ -- Determine if G is isomorphic to a known group of the same size or provide its multiplication table. sorry