PR #18953 feat(zmod/basic)

feat(zmod/basic) #18953

laughinggas wants to merge 9 commits into master from padicint-prop

changed to appropriate locations

3c3cc796

lint error

b27f870f

sorting out linter

9ac75215

github-actions added modifies-synchronized-file

removed references to implicit variables

e594e846

eric-wieser commented on 2023-05-06

added namespace for crt lemmas

3a3ee04d

YaelDillies commented on 2023-05-07

suggested changes 1

0d2f77d3

added discrete topology to mul_opposite

0f52ac63

YaelDillies commented on 2023-05-08

adding additive structure to instance

4a0e970a

eric-wieser commented on 2023-05-08

suggested changes 2

6281a669

YaelDillies commented on 2023-05-08

kim-em added too-late

Reviewers

kbuzzard

YaelDillies

eric-wieser

Assignees

No one assigned

Labels

modifies-synchronized-file too-late

Milestone

No milestone