PR #17201 feat(data/int/gcd): Extended gcds involving 1

feat(data/int/gcd): Extended gcds involving 1 #17201

tb65536 wants to merge 2 commits into master from xgcd_lemmas

lemmas

df8b7abd

tb65536 added awaiting-review

tb65536 changed the title ~~feat(data/int/gcd): Extended gcd of 1~~ feat(data/int/gcd): Extended gcds involving 1 3 years ago

alexjbest commented on 2022-10-28

remove @[simp]

04c72aa7

ocfnash added modifies-synchronized-file

tb65536 removed awaiting-review

kim-em added too-late

Reviewers

alexjbest

Assignees

No one assigned

Labels

modifies-synchronized-file too-late

Milestone

No milestone