Add comm sample
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
Addition commutes — checked on representatives, not inherited from a library.
Proposition
eq (add ⟨1,2⟩ ⟨1,3⟩) (add ⟨1,3⟩ ⟨1,2⟩) ∧ eq (add ⟨3,7⟩ ⟨5,11⟩) (add ⟨5,11⟩ ⟨3,7⟩)Proof
By decide in rational.lean. Checked by the Lean kernel: it depends on no axiom.
Sources and identifiers
- Lean source · src/pair/lean/proofs/rational.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778