Commutative Rings and Modules

This file provides the algebraic foundations for the theory of formal power series (FPS). It corresponds to Section \ref{sec.gf.defs} and \ref{subsec.gf.defs.commrings} of the source material (CommutativeRings.tex).

Overview

Generating functions are not actually functions but formal power series (FPSs). A formal power series is a "formal" infinite sum of the form a₀ + a₁x + a₂x² + ⋯, where x is an indeterminate. Unlike analytic power series, we cannot substitute numerical values for x.

This file reviews the algebraic structures needed for FPS:

• Commutative rings (Definition def.alg.commring)
• Modules over commutative rings (Definition def.alg.module)
• Inverses and fractions in commutative rings (def.commring.inverse, def.commring.fracs)

Structure Note

The TeX source splits ring foundations across two files:

• CommutativeRings.tex: Definitions of commutative rings and modules
• DividingFPS.tex: Inverses, fractions, and FPS-specific division

This Lean file includes the general ring theory from both sources (inverses and fractions) since they are foundational for all subsequent FPS theory. The FPS-specific content (invertibility of power series, Newton's binomial formula, etc.) is in DividingFPS.lean.

Note: The definitions IsInverse, IsInvertible, and fraction here provide a pedagogical bridge between the source's presentation and Mathlib's IsUnit, Units, etc. For actual computations, prefer Mathlib's API directly.

Main Definitions

Definition def.alg.commring (Commutative Ring)

The source defines a commutative ring as a set K with three binary operations (⊕, ⊖, ⊙), two distinguished elements (0 and 1), and nine axioms:

1. Commutativity of addition: a ⊕ b = b ⊕ a
2. Associativity of addition: a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ c
3. Neutrality of zero: a ⊕ 0 = 0 ⊕ a = a
4. Subtraction undoes addition: a ⊕ b = c ↔ a = c ⊖ b
5. Commutativity of multiplication: a ⊙ b = b ⊙ a
6. Associativity of multiplication: a ⊙ (b ⊙ c) = (a ⊙ b) ⊙ c
7. Distributivity: a ⊙ (b ⊕ c) = (a ⊙ b) ⊕ (a ⊙ c) and (a ⊕ b) ⊙ c = (a ⊙ c) ⊕ (b ⊙ c)
8. Neutrality of one: a ⊙ 1 = 1 ⊙ a = a
9. Annihilation: a ⊙ 0 = 0 ⊙ a = 0

In Mathlib, this is captured by CommRing K (from Mathlib.Algebra.Ring.Defs).

Definition def.alg.module (K-Module)

The source defines a K-module as a set M with addition, subtraction, scaling by K, and a zero element, satisfying the standard module axioms.

In Mathlib, this is captured by [AddCommGroup M] [Module K M].

Definition def.commring.inverse (Inverses)

An element a of a commutative ring is invertible (a unit) if there exists b with a * b = 1. The inverse is unique when it exists.

In Mathlib: IsUnit a and Units L (the type Lˣ).

Definition def.commring.fracs (Fractions)

For an invertible element a, we write b/a for b * a⁻¹. Integer powers a^n are defined for all n ∈ ℤ when a is invertible.

In Mathlib: zpow for integer powers on units.

Main Results

Key properties of commutative rings mentioned in the source:

• add_pow: The binomial theorem (a + b)^n = ∑ k, C(n,k) * a^k * b^(n-k)
• sub_pow: Variant for subtraction
• Finite sums and products are well-defined and satisfy standard rules
• isInverse_unique: Inverses are unique (thm.commring.inverse-uni)

Implementation Notes

The source defines commutative rings with explicit subtraction operation ⊖. Mathlib instead defines Ring with negation, and subtraction is derived as a - b := a + (-b). These definitions are equivalent:

• Given subtraction ⊖, define negation as -a := 0 ⊖ a
• Given negation, define subtraction as a - b := a + (-b)

The key theorem commRing_sub_iff_add below shows that Axiom 4 (subtraction undoes addition) holds in Mathlib's formulation.

Similarly, the source defines modules with explicit subtraction, while Mathlib uses negation. The equivalence is analogous.

References

• Source: AlgebraicCombinatorics/tex/FPS/CommutativeRings.tex
• Additional source: AlgebraicCombinatorics/tex/FPS/DividingFPS.tex (inverses/fractions)
• Labels: def.alg.commring, def.alg.module, def.commring.inverse, def.commring.fracs

Section: Commutative Rings

A commutative ring is a set K equipped with operations +, -, * and elements 0, 1 satisfying the standard ring axioms with commutativity of multiplication.

In Mathlib, this is captured by the CommRing typeclass.

theorem AlgebraicCombinatorics.FPS.commRing_add_comm {K : Type u_1} [CommRing K] (a b : K) : a + b = b + a

Commutativity of addition (Axiom 1 in def.alg.commring): a + b = b + a for all a, b ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_add_assoc {K : Type u_1} [CommRing K] (a b c : K) : a + (b + c) = a + b + c

Associativity of addition (Axiom 2 in def.alg.commring): a + (b + c) = (a + b) + c for all a, b, c ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_add_zero {K : Type u_1} [CommRing K] (a : K) : a + 0 = a

Neutrality of zero (Axiom 3 in def.alg.commring): a + 0 = a for all a ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_zero_add {K : Type u_1} [CommRing K] (a : K) : 0 + a = a

Neutrality of zero (Axiom 3 in def.alg.commring): 0 + a = a for all a ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_sub_iff_add {K : Type u_1} [CommRing K] (a b c : K) : a + b = c ↔ a = c - b

Subtraction undoes addition (Axiom 4 in def.alg.commring): a + b = c ↔ a = c - b for all a, b, c ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_mul_comm {K : Type u_1} [CommRing K] (a b : K) : a * b = b * a

Commutativity of multiplication (Axiom 5 in def.alg.commring): a * b = b * a for all a, b ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_mul_assoc {K : Type u_1} [CommRing K] (a b c : K) : a * (b * c) = a * b * c

Associativity of multiplication (Axiom 6 in def.alg.commring): a * (b * c) = (a * b) * c for all a, b, c ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_left_distrib {K : Type u_1} [CommRing K] (a b c : K) : a * (b + c) = a * b + a * c

Distributivity (Axiom 7 in def.alg.commring): a * (b + c) = a * b + a * c for all a, b, c ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_right_distrib {K : Type u_1} [CommRing K] (a b c : K) : (a + b) * c = a * c + b * c

Distributivity (Axiom 7 in def.alg.commring): (a + b) * c = a * c + b * c for all a, b, c ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_mul_one {K : Type u_1} [CommRing K] (a : K) : a * 1 = a

Neutrality of one (Axiom 8 in def.alg.commring): a * 1 = a for all a ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_one_mul {K : Type u_1} [CommRing K] (a : K) : 1 * a = a

Neutrality of one (Axiom 8 in def.alg.commring): 1 * a = a for all a ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_mul_zero {K : Type u_1} [CommRing K] (a : K) : a * 0 = 0

Annihilation (Axiom 9 in def.alg.commring): a * 0 = 0 for all a ∈ K.

theorem AlgebraicCombinatorics.FPS.commRing_zero_mul {K : Type u_1} [CommRing K] (a : K) : 0 * a = 0

Annihilation (Axiom 9 in def.alg.commring): 0 * a = 0 for all a ∈ K.

Section: Examples of Commutative Rings

The source lists several examples of commutative rings:

• ℤ, ℚ, ℝ, ℂ are commutative rings
• ℕ is NOT a commutative ring (no subtraction), but is a commutative semiring
• ℤ[√5] is a commutative ring (subring of ℝ)
• ℤ/m is a commutative ring for any m
• Power set with symmetric difference is a Boolean ring
• The tropical semiring ℤ ∪ {-∞} with max and + operations

In Mathlib, these are available as instances:

• CommRing ℤ, CommRing ℚ, etc.
• CommSemiring ℕ
• ZMod n for ℤ/n

Section: Standard Rules in Commutative Rings

The source notes that in any commutative ring K, the standard rules of computation apply:

• Finite sums are well-defined (general associativity and commutativity)
• Finite products are well-defined
• Standard algebraic identities hold
• The binomial theorem: (a + b)^n = ∑_{k=0}^n C(n,k) * a^k * b^(n-k)

theorem AlgebraicCombinatorics.FPS.neg_add_distrib {K : Type u_1} [CommRing K] (a b : K) : -(a + b) = -a + -b

Negation distributes over addition: -(a + b) = (-a) + (-b).

theorem AlgebraicCombinatorics.FPS.neg_neg_eq {K : Type u_1} [CommRing K] (a : K) : - -a = a

Double negation: -(-a) = a.

theorem AlgebraicCombinatorics.FPS.add_zsmul_distrib {K : Type u_1} [CommRing K] (a : K) (n m : ℤ) : (n + m) • a = n • a + m • a

Scalar multiplication by integers distributes: (n + m) • a = n • a + m • a.

theorem AlgebraicCombinatorics.FPS.mul_zsmul_assoc {K : Type u_1} [CommRing K] (a : K) (n m : ℤ) : (n * m) • a = n • m • a

Scalar multiplication by integers is associative: (n * m) • a = n • (m • a).

theorem AlgebraicCombinatorics.FPS.mul_sub_distrib {K : Type u_1} [CommRing K] (a b c : K) : a * (b - c) = a * b - a * c

Multiplication distributes over subtraction: a * (b - c) = a * b - a * c.

theorem AlgebraicCombinatorics.FPS.mul_pow_eq {K : Type u_1} [CommRing K] (a b : K) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n

Power of a product: (a * b)^n = a^n * b^n.

theorem AlgebraicCombinatorics.FPS.pow_add_eq {K : Type u_1} [CommRing K] (a : K) (n m : ℕ) : a ^ (n + m) = a ^ n * a ^ m

Power addition rule: a^(n+m) = a^n * a^m.

theorem AlgebraicCombinatorics.FPS.pow_mul_eq {K : Type u_1} [CommRing K] (a : K) (n m : ℕ) : a ^ (n * m) = (a ^ n) ^ m

Power multiplication rule: a^(n*m) = (a^n)^m.

theorem AlgebraicCombinatorics.FPS.binomial_theorem {K : Type u_1} [CommRing K] (a b : K) (n : ℕ) : (a + b) ^ n = ∑ k ∈ Finset.range (n + 1), a ^ k * b ^ (n - k) * ↑(n.choose k)

The Binomial Theorem (mentioned in def.alg.commring): (a + b)^n = ∑_{k=0}^n C(n,k) * a^k * b^(n-k).

In Mathlib, this is add_pow from Mathlib.Data.Nat.Choose.Sum.

theorem AlgebraicCombinatorics.FPS.binomial_theorem_sub {K : Type u_1} [CommRing K] (a b : K) (n : ℕ) : (a - b) ^ n = ∑ m ∈ Finset.range (n + 1), (-1) ^ (m + n) * a ^ m * b ^ (n - m) * ↑(n.choose m)

Variant of the binomial theorem with subtraction.

Section: Modules over Commutative Rings

A K-module is a generalization of a vector space where the scalars come from a commutative ring K (not necessarily a field).

The source defines a K-module (Definition def.alg.module) as a set M with:

• Addition ⊕ : M × M → M
• Subtraction ⊖ : M × M → M
• Scaling ⇀ : K × M → M
• Zero element 0⃗ ∈ M

satisfying the standard module axioms.

In Mathlib, this is captured by the Module typeclass, which requires:

• AddCommGroup M (for the additive structure)
• Module K M (for the scalar multiplication)

theorem AlgebraicCombinatorics.FPS.module_add_comm {M : Type u_2} [AddCommGroup M] (a b : M) : a + b = b + a

Commutativity of addition (Axiom 1 in def.alg.module): a + b = b + a for all a, b ∈ M.

theorem AlgebraicCombinatorics.FPS.module_add_assoc {M : Type u_2} [AddCommGroup M] (a b c : M) : a + (b + c) = a + b + c

Associativity of addition (Axiom 2 in def.alg.module): a + (b + c) = (a + b) + c for all a, b, c ∈ M.

theorem AlgebraicCombinatorics.FPS.module_add_zero {M : Type u_2} [AddCommGroup M] (a : M) : a + 0 = a

Neutrality of zero (Axiom 3 in def.alg.module): a + 0 = a for all a ∈ M.

theorem AlgebraicCombinatorics.FPS.module_sub_iff_add {M : Type u_2} [AddCommGroup M] (a b c : M) : a + b = c ↔ a = c - b

Subtraction undoes addition (Axiom 4 in def.alg.module): a + b = c ↔ a = c - b for all a, b, c ∈ M.

theorem AlgebraicCombinatorics.FPS.module_smul_assoc {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (u v : K) (a : M) : u • v • a = (u * v) • a

Associativity of scaling (Axiom 5 in def.alg.module): u • (v • a) = (u * v) • a for all u, v ∈ K and a ∈ M.

theorem AlgebraicCombinatorics.FPS.module_smul_add {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (u : K) (a b : M) : u • (a + b) = u • a + u • b

Left distributivity (Axiom 6 in def.alg.module): u • (a + b) = u • a + u • b for all u ∈ K and a, b ∈ M.

theorem AlgebraicCombinatorics.FPS.module_add_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (u v : K) (a : M) : (u + v) • a = u • a + v • a

Right distributivity (Axiom 7 in def.alg.module): (u + v) • a = u • a + v • a for all u, v ∈ K and a ∈ M.

theorem AlgebraicCombinatorics.FPS.module_one_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (a : M) : 1 • a = a

Neutrality of one (Axiom 8 in def.alg.module): 1 • a = a for all a ∈ M.

theorem AlgebraicCombinatorics.FPS.module_zero_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (a : M) : 0 • a = 0

Left annihilation (Axiom 9 in def.alg.module): 0 • a = 0 for all a ∈ M.

theorem AlgebraicCombinatorics.FPS.module_smul_zero {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (u : K) : u • 0 = 0

Right annihilation (Axiom 10 in def.alg.module): u • 0 = 0 for all u ∈ K.

Additive Inverses and Subtraction

The source notes that most authors do not include subtraction in the definition of a K-module. Instead, additive inverses can be constructed using scaling: the additive inverse of a is (-1) • a. This shows that subtraction is derivable from the other operations.

In Mathlib, AddCommGroup M provides negation directly, and subtraction is defined as a - b := a + (-b). The following theorems show the equivalence between these approaches.

theorem AlgebraicCombinatorics.FPS.module_neg_eq_neg_one_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (a : M) : -a = -1 • a

Additive inverse via scaling (Note in def.alg.module): The additive inverse of a can be constructed as (-1) • a. This shows why modules don't need explicit negation in their axioms.

theorem AlgebraicCombinatorics.FPS.module_sub_eq_add_neg {M : Type u_2} [AddCommGroup M] (a b : M) : a - b = a + -b

Subtraction can be expressed as addition of the negation.

theorem AlgebraicCombinatorics.FPS.module_sub_eq_add_neg_one_smul {K : Type u_1} [CommRing K] {M : Type u_2} [AddCommGroup M] [Module K M] (a b : M) : a - b = a + -1 • b

Subtraction can be expressed using scaling by -1.

theorem AlgebraicCombinatorics.FPS.module_neg_add {M : Type u_2} [AddCommGroup M] (a b : M) : -(a + b) = -a + -b

Negation distributes over addition in a module.

theorem AlgebraicCombinatorics.FPS.module_neg_neg {M : Type u_2} [AddCommGroup M] (a : M) : - -a = a

Double negation in a module.

Section: Module Examples

Any commutative ring K is a module over itself.

Section: Finite Sums and Products

The source emphasizes that finite sums and products in commutative rings are well-defined regardless of the order of operations or placement of parentheses.

In Mathlib, this is captured by Finset.sum and Finset.prod.

theorem AlgebraicCombinatorics.FPS.sum_disjoint_union {K : Type u_1} [CommRing K] {S : Type u_2} [DecidableEq S] {X Y : Finset S} (hXY : Disjoint X Y) (f : S → K) : ∑ s ∈ X ∪ Y, f s = ∑ s ∈ X, f s + ∑ s ∈ Y, f s

Finite sums can be split over disjoint sets.

theorem AlgebraicCombinatorics.FPS.sum_add_distrib' {K : Type u_1} [CommRing K] {S : Type u_2} {T : Finset S} (f g : S → K) : ∑ s ∈ T, (f s + g s) = ∑ s ∈ T, f s + ∑ s ∈ T, g s

Finite sums distribute over addition.

theorem AlgebraicCombinatorics.FPS.sum_empty {K : Type u_1} [CommRing K] {S : Type u_2} (f : S → K) : ∑ _s ∈ ∅, f _s = 0

Empty sum equals zero.

theorem AlgebraicCombinatorics.FPS.prod_empty {K : Type u_1} [CommRing K] {S : Type u_2} (f : S → K) : ∏ _s ∈ ∅, f _s = 1

Empty product equals one.

Section: Inverses in Commutative Rings (def.commring.inverse)

Definition (def.commring.inverse): Let L be a commutative ring. Let a ∈ L. Then:

• (a) An inverse (or multiplicative inverse) of a means an element b ∈ L such that a * b = b * a = 1 (where 1 is the unity of L).

• (b) We say that a is invertible in L (or a unit of L) if a has an inverse.

Note: The condition a * b = b * a = 1 in part (a) can be restated as simply a * b = 1, because we automatically have a * b = b * a (since L is a commutative ring). The source writes a * b = b * a = 1 so that the definition applies verbatim to noncommutative rings as well.

Examples:

• In ℤ, the only invertible elements are 1 and -1. Each is its own inverse.
• In ℚ, ℝ, ℂ (and any field), every nonzero element is invertible.

In Mathlib, this is captured by:

• IsUnit a : the predicate that a is invertible (a unit)
• Lˣ (or Units L) : the type of units of L, which forms a group under multiplication
• For u : Lˣ, we have u⁻¹ : Lˣ (the inverse unit)

Definition def.commring.inverse (a): Inverse of an element

An inverse of a is an element b such that a * b = 1 (and equivalently b * a = 1 in a commutative ring).

def AlgebraicCombinatorics.FPS.IsInverse {L : Type u_1} [CommRing L] (a b : L) : Prop

Definition def.commring.inverse (a): b is an inverse of a if a * b = 1. In a commutative ring, this is equivalent to b * a = 1.

Equations

• AlgebraicCombinatorics.FPS.IsInverse a b = (a * b = 1)

theorem AlgebraicCombinatorics.FPS.isInverse_comm {L : Type u_1} [CommRing L] (a b : L) : IsInverse a b ↔ IsInverse b a

In a commutative ring, IsInverse a b is symmetric: if a * b = 1, then b * a = 1.

theorem AlgebraicCombinatorics.FPS.isInverse_symm {L : Type u_1} [CommRing L] {a b : L} (h : IsInverse a b) : IsInverse b a

The inverse relation is symmetric in commutative rings.

theorem AlgebraicCombinatorics.FPS.isInverse_one_one {L : Type u_1} [CommRing L] : IsInverse 1 1

1 is an inverse of 1.

theorem AlgebraicCombinatorics.FPS.not_isInverse_zero_of_nontrivial {L : Type u_1} [CommRing L] [Nontrivial L] (b : L) : ¬IsInverse 0 b

0 has no inverse (unless L is the trivial ring where 0 = 1).

theorem AlgebraicCombinatorics.FPS.isInverse_unique {L : Type u_1} [CommRing L] {a b c : L} (hab : IsInverse a b) (hac : IsInverse a c) : b = c

If a has an inverse, then a * b = 1 implies b is that inverse. Label: thm.commring.inverse-uni

Definition def.commring.inverse (b): Invertible elements (units)

An element a is invertible (or a unit) if it has an inverse.

def AlgebraicCombinatorics.FPS.IsInvertible {L : Type u_1} [CommRing L] (a : L) : Prop

Definition def.commring.inverse (b): a is invertible if there exists b with a * b = 1. In Mathlib, this is IsUnit a.

Equations

• AlgebraicCombinatorics.FPS.IsInvertible a = ∃ (b : L), AlgebraicCombinatorics.FPS.IsInverse a b

theorem AlgebraicCombinatorics.FPS.isInvertible_iff_isUnit {L : Type u_1} [CommRing L] (a : L) : IsInvertible a ↔ IsUnit a

IsInvertible is equivalent to Mathlib's IsUnit.

theorem AlgebraicCombinatorics.FPS.isInvertible_one {L : Type u_1} [CommRing L] : IsInvertible 1

1 is invertible.

theorem AlgebraicCombinatorics.FPS.not_isInvertible_zero {L : Type u_1} [CommRing L] [Nontrivial L] : ¬IsInvertible 0

0 is not invertible in a nontrivial ring.

theorem AlgebraicCombinatorics.FPS.isInvertible_mul {L : Type u_1} [CommRing L] {a b : L} (ha : IsInvertible a) (hb : IsInvertible b) : IsInvertible (a * b)

The product of two invertible elements is invertible.

theorem AlgebraicCombinatorics.FPS.isInvertible_of_isInverse {L : Type u_1} [CommRing L] {a b : L} (h : IsInverse a b) : IsInvertible b

The inverse of an invertible element is invertible.

Examples of invertible elements

The source gives examples:

• In ℤ, only 1 and -1 are invertible
• In fields (ℚ, ℝ, ℂ), every nonzero element is invertible

theorem AlgebraicCombinatorics.FPS.int_isUnit_iff (n : ℤ) : IsUnit n ↔ n = 1 ∨ n = -1

In ℤ, the only units are 1 and -1.

theorem AlgebraicCombinatorics.FPS.field_isUnit_of_ne_zero {F : Type u_2} [Field F] {a : F} (ha : a ≠ 0) : IsUnit a

In a field, every nonzero element is invertible.

theorem AlgebraicCombinatorics.FPS.field_isUnit_iff {F : Type u_2} [Field F] {a : F} : IsUnit a ↔ a ≠ 0

In a field, a is invertible iff a ≠ 0.

Connection to Mathlib's Units type

In Mathlib, the type Lˣ (or Units L) consists of invertible elements of L. Each u : Lˣ carries both the element and its inverse, and satisfies u * u⁻¹ = 1.

theorem AlgebraicCombinatorics.FPS.units_isInverse {L : Type u_1} [CommRing L] (u : Lˣ) : IsInverse ↑u ↑u⁻¹

Every unit satisfies the inverse property: u * u⁻¹ = 1.

theorem AlgebraicCombinatorics.FPS.units_isInvertible {L : Type u_1} [CommRing L] (u : Lˣ) : IsInvertible ↑u

The coercion from Lˣ to L gives an invertible element.

noncomputable def AlgebraicCombinatorics.FPS.unitOfInverse {L : Type u_1} [CommRing L] {a b : L} (h : IsInverse a b) : Lˣ

Construct a unit from an element and its inverse.

Equations

• AlgebraicCombinatorics.FPS.unitOfInverse h = ⋯.unit

theorem AlgebraicCombinatorics.FPS.unitOfInverse_val {L : Type u_1} [CommRing L] {a b : L} (h : IsInverse a b) : ↑(unitOfInverse h) = a

The constructed unit has the expected value.

Section: Inverses and Fractions in Commutative Rings

Definition (def.commring.fracs): For an invertible element a in a commutative ring L:

• (a) The inverse of a is denoted a⁻¹ (unique by thm.commring.inverse-uni)
• (b) For any b ∈ L, the fraction b/a is defined as b * a⁻¹
• (c) For negative integers n, we define a^n := (a⁻¹)^(-n)

In Mathlib, these are handled via:

• The Units type Lˣ for invertible elements, which forms a group
• Ring.inverse for a partial inverse function on the ring
• Integer powers zpow on units

Part (a): Inverse notation

The inverse of an invertible element a is unique (by inverse_unique / thm.commring.inverse-uni) and is denoted a⁻¹.

In Mathlib, for a general commutative ring:

• Lˣ is the type of units (invertible elements) of L
• For u : Lˣ, we have u⁻¹ : Lˣ (the inverse unit)
• Ring.inverse a gives a⁻¹ if a is a unit, and 0 otherwise

theorem AlgebraicCombinatorics.FPS.unit_mul_inv {L : Type u_1} [CommRing L] (u : Lˣ) : ↑u * ↑u⁻¹ = 1

For a unit u, the inverse satisfies u * u⁻¹ = 1. Label: def.commring.fracs (a)

theorem AlgebraicCombinatorics.FPS.unit_inv_mul {L : Type u_1} [CommRing L] (u : Lˣ) : ↑u⁻¹ * ↑u = 1

For a unit u, the inverse satisfies u⁻¹ * u = 1. Label: def.commring.fracs (a)

theorem AlgebraicCombinatorics.FPS.inverse_unique' {L : Type u_1} [CommRing L] {a b c : L} (hb : a * b = 1) (hc : a * c = 1) : b = c

The inverse of a unit is unique: if a * b = 1 and a * c = 1, then b = c. This is thm.commring.inverse-uni from the source. Label: def.commring.fracs (a)

Part (b): Fraction notation

For any b ∈ L and invertible a ∈ L, we define b/a := b * a⁻¹.

In Mathlib, for a unit u : Lˣ and element b : L:

• We can write b * (u⁻¹ : L) or equivalently b / u when appropriate coercions exist

def AlgebraicCombinatorics.FPS.fraction {L : Type u_1} [CommRing L] (b : L) (u : Lˣ) : L

The fraction b/a is defined as b * a⁻¹ for a unit a. Label: def.commring.fracs (b)

Note: This is equivalent to AlgebraicCombinatorics.divByUnit in DividingFPS.lean. Both definitions exist for pedagogical reasons: this file provides foundational ring theory, while DividingFPS.lean focuses on FPS-specific applications.

Equations

• AlgebraicCombinatorics.FPS.fraction b u = b * ↑u⁻¹

theorem AlgebraicCombinatorics.FPS.fraction_eq_divByUnit {L : Type u_1} [CommRing L] (b : L) (u : Lˣ) : fraction b u = divByUnit b u

Bridge lemma: fraction is definitionally equal to divByUnit. This connects the pedagogical definition in this file to the one in DividingFPS.lean.

theorem AlgebraicCombinatorics.FPS.fraction_eq_iff {L : Type u_1} [CommRing L] (b c : L) (u : Lˣ) : fraction b u = c ↔ b = c * ↑u

Alternative characterization: b/a = c iff b = c * a. Label: def.commring.fracs (b)

theorem AlgebraicCombinatorics.FPS.fraction_one {L : Type u_1} [CommRing L] (u : Lˣ) : fraction 1 u = ↑u⁻¹

Fraction of 1 equals the inverse: 1/a = a⁻¹. Label: def.commring.fracs (b)

theorem AlgebraicCombinatorics.FPS.fraction_unit_one {L : Type u_1} [CommRing L] (b : L) : fraction b 1 = b

Fraction with identity denominator: b/1 = b. Label: def.commring.fracs (b)

Part (c): Negative powers

For an invertible element a and negative integer n, we define a^n := (a⁻¹)^(-n). Thus a^n is defined for all n ∈ ℤ.

In Mathlib, for u : Lˣ, integer powers are defined via zpow:

• u ^ (n : ℤ) for any integer n
• For negative n, this is (u⁻¹) ^ (-n)

theorem AlgebraicCombinatorics.FPS.unit_zpow_neg {L : Type u_1} [CommRing L] (u : Lˣ) (n : ℕ) : u ^ (-↑n) = u⁻¹ ^ n

For a unit, u^(-n) = (u⁻¹)^n for any natural number n. This is the definition of negative powers. Label: def.commring.fracs (c)

theorem AlgebraicCombinatorics.FPS.unit_zpow_neg_one {L : Type u_1} [CommRing L] (u : Lˣ) : u ^ (-1) = u⁻¹

For a unit, u^(-1) = u⁻¹. Label: def.commring.fracs (c)

theorem AlgebraicCombinatorics.FPS.unit_zpow_add {L : Type u_1} [CommRing L] (u : Lˣ) (m n : ℤ) : u ^ (m + n) = u ^ m * u ^ n

Power addition rule extends to integer exponents: u^(m+n) = u^m * u^n. Label: def.commring.fracs (c)

theorem AlgebraicCombinatorics.FPS.unit_zpow_mul {L : Type u_1} [CommRing L] (u : Lˣ) (m n : ℤ) : (u ^ m) ^ n = u ^ (m * n)

Power of power rule for integer exponents: (u^m)^n = u^(m*n). Label: def.commring.fracs (c)

theorem AlgebraicCombinatorics.FPS.unit_inv_zpow {L : Type u_1} [CommRing L] (u : Lˣ) (n : ℤ) : (u ^ n)⁻¹ = u ^ (-n)

Inverse of a power: (u^n)⁻¹ = u^(-n). Label: def.commring.fracs (c)