Skip to content

A lean 4 proof of unique prime factorization in well-ordered rings, starting from ring axioms.

Notifications You must be signed in to change notification settings

cymcymcymcym/Unique_Factorization_Lean4

Repository files navigation

About

A lean 4 proof of unique prime factorization in well-ordered rings, starting from ring axioms.

Resources

Stars

Watchers

Forks

Languages