C09 — Groups and Rings: Summary Notes

Table of Contents

• Part I — Groups (S01)
  • Monoids
  • Homomorphisms of Monoids and Groups
    • Monoid homomorphisms
    • Groups and the group/abel tactics
    • Group homomorphisms
  • Group Isomorphisms
  • Subgroups
    • Closure properties
    • Example: ℤ as an additive subgroup of ℚ
    • A subgroup is itself a group
    • Lattice operations on subgroups
    • Conjugate subgroups
  • Homomorphisms Acting on Subgroups
    • Image (map) and preimage (comap)
    • Kernel and range membership
    • Monotonicity of map and comap
    • map/comap along a composition
  • Counting: Lagrange and Sylow
    • Lagrange's theorem
    • Sylow's theorem
    • Triviality via cardinality
  • Quotient Groups
    • Normal subgroups and the quotient group
    • Universal properties: lift, map, and friends
  • A Chinese-Remainder-Style Finale
    • Auxiliary cardinality lemma
    • First isomorphism: K ≃* G ⧸ H
    • Second isomorphism: G ≃* (G ⧸ K) × (G ⧸ H)
    • Final isomorphism: G ≃* H × K
• Part II — Rings (S02)
  • Units of a Ring
  • Quotient Rings
    • The quotient projection
    • Universal properties: lift and quotientMap
    • First isomorphism theorem for rings
  • Ideal Arithmetic
  • Polynomial Rings
    • The embedding C and the indeterminate X
    • Degrees
    • Evaluation and roots

Merged chapter note, generated from the per-section notes C09-S01.md, C09-S02.md, which remain available alongside this file.

Part I — Groups (S01)

Summary generated from the comments in C09-S01.lean.

Monoids

Class	Definition	Key lemma
Monoid	a Semigroup with identity 1 such that x * 1 = x and 1 * x = x	mul_one, one_mul
AddCommMonoid	an AddMonoid with commutative addition	add_comm

example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x
example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y

Homomorphisms of Monoids and Groups

Monoid homomorphisms

A homomorphism of (multiplicative) monoids, written f : M →* N, preserves multiplication and the identity; additive monoid homomorphisms are written f : M →+ N:

example {M N : Type*} [Monoid M] [Monoid N] (x y : M) (f : M →* N) : f (x * y) = f x * f y :=
  f.map_mul x y
example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 :=
  f.map_zero

Composition of (additive) monoid homomorphisms is given by g.comp f:

example {M N P : Type*} [AddMonoid M] [AddMonoid N] [AddMonoid P]
    (f : M →+ N) (g : N →+ P) : M →+ P := g.comp f

Groups and the group/abel tactics

A Group is a monoid with inverses; an AddCommGroup is the additive, commutative counterpart.

Tactic	Scope
group	proves identities true in any group (free-group normalization)
abel	proves identities true in any abelian (additive commutative) group

example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_cancel x
example {G : Type*} [Group G] (x y z : G) : x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
  group
example {G : Type*} [AddCommGroup G] (x y z : G) : z + x + (y - z - x) = y := by
  abel

TIP

group and abel are huge time-savers for "obvious" rearrangements — use them instead of hand-chaining associativity/inverse lemmas.

Group homomorphisms

Homomorphisms of (multiplicative) groups are monoid homomorphisms; they automatically preserve inverses:

Lemma	Statement
f.map_mul	f (x * y) = f x * f y
f.map_inv	f (x⁻¹) = (f x)⁻¹

Conversely, a bare function that preserves multiplication between groups is enough to build a homomorphism — preservation of 1 and ⁻¹ comes for free:

example {G H : Type*} [Group G] [Group H] (f : G → H) (h : ∀ x y, f (x * y) = f x * f y) :
    G →* H :=
  MonoidHom.mk' f h

Group Isomorphisms

A group isomorphism f : G ≃* H is a bijective homomorphism bundled with its inverse (MulEquiv).

• Composing with the symmetric gives the identity isomorphism:

  example {G H : Type*} [Group G] [Group H] (f : G ≃* H) :
      f.trans f.symm = MulEquiv.refl G :=
    f.self_trans_symm

• A bijective homomorphism upgrades to an isomorphism:

  noncomputable example {G H : Type*} [Group G] [Group H]
      (f : G →* H) (h : Function.Bijective f) : G ≃* H :=
    MulEquiv.ofBijective f h

Subgroups

Closure properties

A subgroup H : Subgroup G is closed under the group operations:

Closure	Lemma	Statement
multiplication	H.mul_mem	x ∈ H → y ∈ H → x * y ∈ H
inverses	H.inv_mem	x ∈ H → x⁻¹ ∈ H

Example: ℤ as an additive subgroup of ℚ

example : AddSubgroup ℚ where
  carrier := Set.range ((↑) : ℤ → ℚ)
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  neg_mem' := by
    rintro _ ⟨n, rfl⟩
    use -n
    simp

Field	Role	Proof idea
carrier	the underlying set: Set.range ((↑) : ℤ → ℚ), the image of the coercion ℤ → ℚ	the coercion is an enforced conversion — since the ambient group is ℚ, the carrier must be a subset of ℚ
add_mem'	closure under +	destruct as ↑n, ↑m; witness ↑(n + m); simp since (↑) preserves addition
zero_mem'	0 ∈ carrier	witness 0 = ↑0
neg_mem'	closure under negation	witness -(↑n) = ↑(-n)

A subgroup is itself a group

example {G : Type*} [Group G] (H : Subgroup G) : Group H := inferInstance
example {G : Type*} [Group G] (H : Subgroup G) : Group {x : G // x ∈ H} := inferInstance

H (as a Subgroup G) and the subtype {x : G // x ∈ H} carry the same Group instance.

Lattice operations on subgroups

• Infimum is literal intersection of the underlying sets:

  example {G : Type*} [Group G] (H H' : Subgroup G) :
      ((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl

• Supremum is the subgroup generated by the union of the underlying sets:

  example {G : Type*} [Group G] (H H' : Subgroup G) :
      ((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G)) := by
    rw [Subgroup.sup_eq_closure]

• Top and bottom: x ∈ (⊤ : Subgroup G) holds trivially for every x; x ∈ (⊥ : Subgroup G) ↔ x = 1 (Subgroup.mem_bot).

WARNING

Just as for submodules, the set-theoretic union of two subgroups is generally not a subgroup — ⊔ closes it up via Subgroup.closure.

Conjugate subgroups

The conjugate of a subgroup H by an element x is the subgroup x H x⁻¹:

Full definition and proof walkthrough (click to expand)

def conjugate {G : Type*} [Group G] (x : G) (H : Subgroup G) : Subgroup G where
  carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}
  one_mem' := by
    dsimp
    use 1
    constructor
    exact H.one_mem
    group
  inv_mem' := by
    dsimp
    rintro - ⟨h, h_in, rfl⟩
    use h⁻¹, H.inv_mem h_in
    group
  mul_mem' := by
    dsimp
    rintro - - ⟨h, h_in, rfl⟩ ⟨k, k_in, rfl⟩
    use h*k, H.mul_mem h_in k_in
    group

Each obligation follows the same pattern: unfold the carrier with dsimp, destruct the existential to expose an element of H, supply the corresponding element of H as witness (1, h⁻¹, h * k), and let the group tactic discharge the pure group identity — e.g. x * 1 * x⁻¹ = 1, (x * h * x⁻¹)⁻¹ = x * h⁻¹ * x⁻¹, and (x * h * x⁻¹) * (x * k * x⁻¹) = x * (h * k) * x⁻¹.

Homomorphisms Acting on Subgroups

Let f : G →* H be a group homomorphism.

Image (map) and preimage (comap)

example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
  Subgroup.map f G'
example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G :=
  Subgroup.comap f H'

• Subgroup.map f G' — the image of a subgroup of the source, a subgroup of the target.
• Subgroup.comap f H' — the preimage of a subgroup of the target, a subgroup of the source.

Kernel and range membership

Lemma	Statement
f.mem_ker	g ∈ MonoidHom.ker f ↔ f g = 1
f.mem_range	h ∈ MonoidHom.range f ↔ ∃ g : G, f g = h

Monotonicity of map and comap

Both operations are monotone:

example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
  intro x hx
  rw [mem_comap] at * -- Lean does not need this line
  exact hST hx

example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T := by
  intro x hx
  rw [mem_map] at * -- Lean does not need this line
  rcases hx with ⟨y, hy, rfl⟩
  use y, hST hy

The rw [mem_comap]/rw [mem_map] lines are only for readability — membership in comap/map is already definitional, so Lean does not need them.

map/comap along a composition

Pullback is contravariant, pushforward is covariant:

$$\mathrm{comap}(\psi \circ \phi )=\mathrm{comap}\phi \circ \mathrm{comap}\psi ,\mathrm{map}(\psi \circ \phi )=\mathrm{map}\psi \circ \mathrm{map}\phi$$

Proofs (click to expand)

example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
    comap (ψ.comp φ) U = comap φ (comap ψ U) := by
  ext x
  simp only [mem_comap]
  rfl

example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
    map (ψ.comp φ) S = map ψ (S.map φ) := by
  ext x
  simp only [mem_map]
  constructor
  · rintro ⟨y, y_in, hy⟩
    exact ⟨φ y, ⟨y, y_in, rfl⟩, hy⟩
  · rintro ⟨y, ⟨z, z_in, hz⟩, hy⟩
    use z, z_in
    calc ψ.comp φ z = ψ (φ z) := rfl
    _               = ψ y := by congr
    _               = x := hy

• The comap identity is true by definition — ext + simp only [mem_comap] + rfl (the whole proof could be a single rfl).
• For map, both directions chase the existentials: the forward direction maps the witness through φ; the backward direction unpacks the nested witness and finishes with a calc chain, using congr to rewrite with hz : φ z = y inside ψ.

Counting: Lagrange and Sylow

Lagrange's theorem

The cardinality of a subgroup divides the cardinality of the whole group:

$$|G^{\prime }|||G|,\text{i.e. }\mathrm{\exists }k,|G|=|G^{\prime }|\cdot k$$

where the witness k is the index G'.index of the subgroup:

example {G : Type*} [Group G] (G' : Subgroup G) : Nat.card G' ∣ Nat.card G :=
  ⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩

The anonymous constructor provides the existential witness G'.index; h ▸ e rewrites e using the equality h, here commuting the product in G'.index_mul_card : G'.index * Nat.card G' = Nat.card G.

Sylow's theorem

For a finite group G and a prime p, if p ^ n ∣ Nat.card G then there is a subgroup of order p ^ n:

example {G : Type*} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact p.Prime]
    (hdvd : p ^ n ∣ Nat.card G) : ∃ K : Subgroup G, Nat.card K = p ^ n :=
  Sylow.exists_subgroup_card_pow_prime p hdvd

Triviality via cardinality

A subgroup is trivial iff its cardinality is 1:

$$H=\mathrm{\perp }⟺|H|=1$$

Proof of `eq_bot_iff_card` (click to expand)

lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} :
    H = ⊥ ↔ Nat.card H = 1 := by
  suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
    simpa [eq_bot_iff_forall, Nat.card_eq_one_iff_exists]
  constructor
  · intro h
    use 1, H.one_mem
  · rintro ⟨y, -, hy'⟩ x hx
    calc x = y := hy' x hx
    _      = 1 := (hy' 1 H.one_mem).symm

The suffices rephrases both sides as "all elements equal 1" ↔ "all elements equal some common element"; simpa bridges with eq_bot_iff_forall and Nat.card_eq_one_iff_exists. The forward direction uses 1 as the common element; the backward direction shows every x equals the common y, which itself equals 1 (since 1 ∈ H).

Two corollaries of Lagrange-style reasoning:

Lemma	Statement
card_dvd_of_le	if H ≤ K then Nat.card H ∣ Nat.card K
inf_bot_of_coprime (below)	coprime cardinalities force trivial intersection

lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
  have D₁ : Nat.card (H ⊓ K : Subgroup G) ∣ Nat.card H := card_dvd_of_le inf_le_left
  have D₂ : Nat.card (H ⊓ K : Subgroup G) ∣ Nat.card K := card_dvd_of_le inf_le_right
  exact eq_bot_iff_card.2 (Nat.eq_one_of_dvd_coprimes h D₁ D₂)

Since H ⊓ K ≤ H and H ⊓ K ≤ K, its cardinality divides both |H| and |K|; coprimality forces that divisor to be 1, and eq_bot_iff_card finishes.

Quotient Groups

Normal subgroups and the quotient group

H.Normal marks a subgroup that is invariant under conjugation by all group elements — exactly the condition for the quotient to carry a group structure:

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : Group (G ⧸ H) := inferInstance

QuotientGroup.mk' is the canonical projection G →* G ⧸ H:

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : G →* G ⧸ H :=
  QuotientGroup.mk' H

Universal properties: lift, map, and friends

Construction	Type	Requirement
QuotientGroup.lift N φ h	G ⧸ N →* M	h : N ≤ MonoidHom.ker φ — φ kills N
QuotientGroup.quotientKerEquivRange φ	G ⧸ ker φ →* MonoidHom.range φ	— (first isomorphism theorem)
QuotientGroup.map N N' φ h	G ⧸ N →* G' ⧸ N'	h : N ≤ Subgroup.comap φ N' — φ maps N into N'
QuotientGroup.quotientMulEquivOfEq h	G ⧸ M ≃* G ⧸ N	h : M = N

The first isomorphism theorem for groups:

$$G/\ker \phi \cong \mathrm{range}\phi$$

A Chinese-Remainder-Style Finale

Setup. H K : Subgroup G are both normal, G is a Fintype, and:

variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K)
  (h' : Nat.card G = Nat.card H * Nat.card K)

That is, H and K are disjoint and their orders multiply to the order of G. The goal: decompose G as the product H × K.

Auxiliary cardinality lemma

Under Nat.card G = Nat.card H * Nat.card K, the quotient has the complementary cardinality:

lemma aux_card_eq [Finite G] (h' : Nat.card G = Nat.card H * Nat.card K) :
    Nat.card (G ⧸ H) = Nat.card K := by
  have := calc
    Nat.card (G ⧸ H) * Nat.card H = Nat.card G := by rw [← H.index_eq_card, H.index_mul_card]
    _                             = Nat.card K * Nat.card H := by rw [h', mul_comm]
  exact Nat.eq_of_mul_eq_mul_right Nat.card_pos this

Key facts used:

Lemma	Statement
Subgroup.index_eq_card	the index of H equals the cardinality of G ⧸ H
Subgroup.index_mul_card	index H * Nat.card H = Nat.card G
Nat.eq_of_mul_eq_mul_right	cancel a positive right factor (Nat.card_pos supplies positivity)

First isomorphism: K ≃* G ⧸ H

Proof walkthrough (click to expand)

def iso₁ : K ≃* G ⧸ H := by
  apply MulEquiv.ofBijective ((QuotientGroup.mk' H).restrict K)
  rw [Nat.bijective_iff_injective_and_card]
  constructor
  · rw [← ker_eq_bot_iff, (QuotientGroup.mk' H).ker_restrict K]
    simp [h]
  · symm
    exact aux_card_eq h'

1. Candidate map. Restrict the canonical projection QuotientGroup.mk' H : G →* G ⧸ H to the subgroup K (restrict K).
2. Bijectivity by injectivity + cardinality (Nat.bijective_iff_injective_and_card): a map between finite types of equal cardinality is bijective iff injective.
3. Injectivity. ← ker_eq_bot_iff turns it into triviality of the kernel; ker_restrict rewrites the kernel of the restriction as ker (mk' H) viewed as a subgroup of K (subgroupOf), and simp [h] collapses it to ⊥ using disjointness of H and K.
4. Cardinality. aux_card_eq h' gives Nat.card (G ⧸ H) = Nat.card K, symmetrized to match the goal.

Second isomorphism: G ≃* (G ⧸ K) × (G ⧸ H)

Proof walkthrough (click to expand)

def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) := by
  apply MulEquiv.ofBijective <| (QuotientGroup.mk' K).prod (QuotientGroup.mk' H)
  rw [Nat.bijective_iff_injective_and_card]
  constructor
  · rw [← ker_eq_bot_iff, ker_prod]
    simp [h.symm.eq_bot]
  · rw [Nat.card_prod]
    rw [aux_card_eq h', aux_card_eq (mul_comm (Nat.card H) _▸ h'), h']

1. Candidate map. The product of the two projections, g ↦ (gK, gH), via MonoidHom.prod.
2. Injectivity. The kernel of a product map is the intersection of the kernels (ker_prod): ker (mk' K) ⊓ ker (mk' H) = K ⊓ H = ⊥ by disjointness (h.symm.eq_bot).
3. Cardinality. Nat.card_prod splits the product cardinality; both quotient cardinalities evaluate via aux_card_eq — the second applied to h' with the factors commuted — and h' itself closes the equation.

Final isomorphism: G ≃* H × K

Compose iso₂ with the (symmetric of the) product of the two iso₁ isomorphisms — one per factor — using MulEquiv.prodCongr to work componentwise:

def finalIso : G ≃* H × K :=
  (iso₂ h h').trans ((iso₁ h.symm (mul_comm (Nat.card H) _ ▸ h')).prodCongr (iso₁ h h')).symm

$$G\stackrel{\sim }{\to }(G/K)\times (G/H)\stackrel{\sim }{\to }H\times K$$

NOTE

The symmetry bookkeeping: iso₁ h h' : K ≃* G ⧸ H, while iso₁ h.symm (mul_comm .. ▸ h') : H ≃* G ⧸ K. Their prodCongr gives H × K ≃* (G ⧸ K) × (G ⧸ H), and .symm orients it correctly for trans after iso₂.

---

Part II — Rings (S02)

Note on the ring section of Chapter 09, rewritten from the original ch09.md.

Units of a Ring

For a monoid M, Mˣ (Units M) is the type of invertible elements.

Fact	Lemma	Statement
The units of ℤ are exactly 1 and -1	Int.units_eq_one_or	x = 1 ∨ x = -1 for x : ℤˣ
A unit times its inverse is one	Units.mul_inv	(x : M) * x⁻¹ = 1
The units form a group	(instance)	Group Mˣ
Ring homomorphisms act on units	Units.map	f : R →+* S induces Rˣ →* Sˣ

example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x
example {M : Type*} [Monoid M] (x : Mˣ) : (x : M) * x⁻¹ = 1 := Units.mul_inv x
example {M : Type*} [Monoid M] : Group Mˣ := inferInstance
example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) : Rˣ →* Sˣ := Units.map f

NOTE

Monoid is multiplicative by default, so the group structure on Mˣ is multiplicative, and the induced map on units is a monoid homomorphism →*.

Quotient Rings

Let R be a commutative ring and I : Ideal R.

The quotient projection

Ideal.Quotient.mk I : R →+* R ⧸ I is the canonical ring homomorphism onto the quotient ring — the ring analogue of QuotientGroup.mk:

example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R ⧸ I :=
  Ideal.Quotient.mk I

Its kernel is exactly I — an element maps to zero in the quotient iff it lies in the ideal:

$${\mathsf{mk}}_I(a)=0⟺a\in I$$

example {R : Type*} [CommRing R] {a : R} {I : Ideal R} :
    Ideal.Quotient.mk I a = 0 ↔ a ∈ I :=
  Ideal.Quotient.eq_zero_iff_mem

Universal properties: lift and quotientMap

• Lifting. If I ≤ RingHom.ker f (the ideal dies under f), then f factors through the quotient:

  example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (f : R →+* S)
      (H : I ≤ RingHom.ker f) : R ⧸ I →+* S :=
    Ideal.Quotient.lift I f H

• Mapping quotients. If I ≤ Ideal.comap f J (the image of I lands in J), then f descends to a map of quotients:

  example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R →+* S)
      (H : I ≤ Ideal.comap f J) : R ⧸ I →+* S ⧸ J :=
    Ideal.quotientMap J f H

  Why the quotient map is well-defined (click to expand)

  By the definition of comap, ∀ x ∈ I, f x ∈ J, i.e. f(I) ⊆ J. Define the lift by sending each coset x + I to f x + J. If x + I = y + I, then x - y ∈ I, hence f (x - y) = f x - f y ∈ J, which gives f x + J = f y + J.

• Equal ideals give isomorphic quotients:

  example {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
    Ideal.quotEquivOfEq h

  Since I = J, the cosets coincide, so x + I ↦ x + J is an isomorphism — well-defined because x + I = y + I implies x - y ∈ I = J, hence x + J = y + J.

First isomorphism theorem for rings

$$R/\ker f\cong \mathrm{im}f$$

example {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) :
    R ⧸ RingHom.ker f ≃+* f.range :=
  RingHom.quotientKerEquivRange f

Ideal Arithmetic

Let I J : Ideal R for a commutative ring R.

Sum. Elements of I + J are sums of an element of I and an element of J:

example {x : R} : x ∈ I + J ↔ ∃ a ∈ I, ∃ b ∈ J, a + b = x := by
  simp [Submodule.mem_sup]

Product. The product ideal I * J is contained in each factor, and hence in their intersection:

Lemma	Statement	Why
Ideal.mul_le_left	I * J ≤ J	for every x ∈ R, x * J ⊆ J; since I ⊆ R, also ∀ x ∈ I, x * J ⊆ J
Ideal.mul_le_right	I * J ≤ I	symmetrically, ∀ y ∈ R, I * y ⊆ I, so ∀ y ∈ J, I * y ⊆ I
Ideal.mul_le_inf	I * J ≤ I ⊓ J	combining both: every z ∈ I * J lies in both I and J

$$I\cdot J\subseteq I\cap J$$

Polynomial Rings

For a commutative ring R, the polynomial ring R[X] is again a commutative ring.

The embedding C and the indeterminate X

C : R →+* R[X] is the canonical embedding sending r to the constant polynomial; X is the indeterminate.

-- `C r` is the constant polynomial with value `r`
example {R : Type*} [CommRing R] (r : R) := X - C r

-- `C` is a ring homomorphism, so `(C r)^2 = C (r^2)`
example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X ^ 2 - C (r ^ 2) := by
  rw [C.map_pow]
  ring

-- Coefficients are computed with `Polynomial.coeff`
example {R : Type*} [CommRing R] (r : R) : (C r).coeff 0 = r := by simp
example {R : Type*} [CommRing R] : (X ^ 2 + 2 * X + C 3 : R[X]).coeff 1 = 2 := by simp

The coefficient of the constant polynomial C r is r, and the coefficient of X in X ^ 2 + 2 * X + C 3 is 2.

Degrees

Over a semiring with no zero divisors, degree behaves as expected:

Lemma	Statement
Polynomial.degree_mul	degree (p * q) = degree p + degree q
Polynomial.natDegree_comp	natDegree (comp p q) = natDegree p * natDegree q

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    degree (p * q) = degree p + degree q :=
  Polynomial.degree_mul

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    natDegree (comp p q) = natDegree p * natDegree q :=
  Polynomial.natDegree_comp

WARNING

NoZeroDivisors is essential here: if R has zero divisors, leading coefficients can cancel and the degree of a product can drop.

Evaluation and roots

• Evaluation. P.eval x : R evaluates a polynomial at a ring element:

  example {R : Type*} [CommRing R] (P : R[X]) (x : R) := P.eval x

• Roots. r is a root of P iff the evaluation vanishes:

  $$\mathsf{IsRoot}(P,r)⟺P(r)=0$$

  example {R : Type*} [CommRing R] (P : R[X]) (r : R) : IsRoot P r ↔ P.eval r = 0 := Iff.rfl

• Roots of X - C r. Over an integral domain, the linear polynomial X - C r has exactly the root r:

  example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} :=
    roots_X_sub_C r

  Indeed X - C r = 0 forces X = C r, so r is the only solution.

  IMPORTANT

  IsDomain R (a commutative ring with no zero divisors) is necessary for .roots, which relies on the theorem that a nonzero polynomial of degree n has at most n roots in an integral domain.

• Repeated roots. .roots returns a multiset; the roots of (X - C r) ^ n are r with multiplicity n:

  example {R : Type*} [CommRing R] [IsDomain R] (r : R) (n : ℕ) :
      ((X - C r) ^ n).roots = n • {r} := by
    simp

  Here n • {r} denotes the multiset containing r with multiplicity n (• is the SMul operator on multisets).