Zulip Chat Archive

Stream: new members

Topic: Fundamental Theorem of Arithmetic


view this post on Zulip Kevin Buzzard (Oct 21 2019 at 15:52):

(deleted)

view this post on Zulip Leonid Kimelfeld (Oct 29 2019 at 21:14):

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

view this post on Zulip Kevin Buzzard (Oct 29 2019 at 21:19):

Yes.

view this post on Zulip Kevin Buzzard (Oct 29 2019 at 21:22):

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

view this post on Zulip Leonid Kimelfeld (Oct 29 2019 at 21:29):

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

Thank you!

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Jan 03 2020 at 19:21):

(deleted)

view this post on Zulip 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: May 10 2021 at 19:16 UTC