PR #13313 feat(data/nat/sqrt0): Add sqrt0

feat(data/nat/sqrt0): Add sqrt0 #13313

khwilson wants to merge 1 commit into master from add_sqrt0

feat(data/nat/sqrt0): Add sqrt0

dfbf30d1

khwilson added blocked-by-other-PR

leanprover-community-bot-assistant removed blocked-by-other-PR

leanprover-community-bot-assistant added blocked-by-other-PR

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR too-late

Milestone

No milestone