Zulip Chat Archive

Stream: new members

Topic: Fundamental Theorem of Arithmetic

Kevin Buzzard (Oct 21 2019 at 15:52):

(deleted)

Leonid Kimelfeld (Oct 29 2019 at 21:14):

Hi. Is Fundamental theorem of arithmetic (AKA unique factorization theorem) formalized in Lean ?

Kevin Buzzard (Oct 29 2019 at 21:19):

Yes.

Kevin Buzzard (Oct 29 2019 at 21:22):

https://github.com/leanprover-community/mathlib/blob/6030ff0a9d2498b1389c7a3be9b3d938a351dac3/src/data/nat/prime.lean#L415

Leonid Kimelfeld (Oct 29 2019 at 21:29):

https://github.com/leanprover-community/mathlib/blob/6030ff0a9d2498b1389c7a3be9b3d938a351dac3/src/data/nat/prime.lean#L415

Thank you!

Bryan Gin-ge Chen (Oct 29 2019 at 21:32):

See also the discussion on the "100 theorems" branch, which includes some other highlights. @Floris van Doorn Maybe this can be PR'd?

Leonid Kimelfeld (Oct 29 2019 at 21:37):

See also the discussion on the "100 theorems" branch, which includes some other highlights. Floris van Doorn Maybe this can be PR'd?

Interesting!

Kevin Buzzard (Jan 03 2020 at 19:21):

(deleted)

Floris van Doorn (Feb 04 2020 at 17:07):

This was on my todo list for way too long, but I now refer on the 100 theorems branch to the theorem about natural numbers.

Last updated: Dec 20 2023 at 11:08 UTC