λleanlab

Algebra & fields

A ring with zero divisors

Addition and multiplication can obey ring laws even when division by a nonzero element is impossible.

Open Rings.lean in editor
-- A ring with zero divisors
-- History: Modern algebra · finite residue rings.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Modulo 6, the nonzero elements 2 and 3 multiply to zero.
-- Scope: Checks commutative ring laws on every element of Fin 6, and exhibits a zero divisor. These are concrete laws, not a Mathlib typeclass instance.
-- Source: https://lean-lang.org/doc/api/Init/Data/Fin/Basic.html

abbrev R := Fin 6

-- Exhaustive finite proofs are checked by Lean's kernel.
example : ∀ a b c : R, (a+b)+c = a+(b+c) := by decide
example : ∀ a b : R, a+b = b+a := by decide
example : ∀ a : R, a+0 = a := by decide
example : ∀ a : R, a+(-a) = 0 := by decide
example : ∀ a b c : R, (a*b)*c = a*(b*c) := by decide
example : ∀ a b : R, a*b = b*a := by decide
example : ∀ a : R, a*1 = a := by decide
example : ∀ a b c : R, a*(b+c) = a*b+a*c := by decide
example : (0 : R) ≠ 1 := by decide

-- A field would not allow this.
example : (2 : R) ≠ 0 ∧ (3 : R) ≠ 0 ∧ (2 : R)*3 = 0 := by decide
#eval (2 : R)*3

Explanation

theorem / example

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

decide

Builds a proof using a decision procedure. Quantifying over Fin n checks every one of its finitely many values.

Fin n

Fin n contains the natural numbers less than n, each with a bound proof. Addition and multiplication wrap modulo n.

Background and proof scope

Modern algebra · finite residue rings

Modulo 6, the nonzero elements 2 and 3 multiply to zero.

Checks commutative ring laws on every element of Fin 6, and exhibits a zero divisor. These are concrete laws, not a Mathlib typeclass instance.

Lean’s finite residue arithmetic

Expected output

Reference only. Run the file to check its actual result.

0

Exercise

Change the modulus to 5. Which last claim stops being true?