Kevin Buzzard e55da341a6 fix: remove dot notation on MyNat.succ (#119)

2025-09-28 10:40:24 +02:00

..

Addition.lean

Replace recursive definitions of algebraic operations with axioms (#41)

2023-11-22 09:26:49 +01:00

DecidableEq.lean

do not import all of mathlib

2024-03-14 10:38:03 +01:00

DecidableTests.lean

Replace recursive definitions of algebraic operations with axioms (#41)

2023-11-22 09:26:49 +01:00

Definition.lean

fix: remove dot notation on MyNat.succ (#119)

2025-09-28 10:40:24 +02:00

Inequality.lean

big refactor

2023-05-15 15:12:35 +02:00

LE.lean

doc: add historical comments about definition of LE.

2025-03-14 17:06:32 +00:00

Multiplication.lean

Replace recursive definitions of algebraic operations with axioms (#41)

2023-11-22 09:26:49 +01:00

PeanoAxioms.lean

remove import Mathlib.Tactic

2024-12-19 19:41:23 +00:00

Power.lean

fix pretty-printing of Power. #46

2023-12-15 15:22:45 +01:00

TutorialLemmas.lean

sort out succ_eq_add_one import issue for hopefully the last time

2023-09-26 14:13:41 +01:00