polynomial): Modules over `R[X]`
#14666

Open

feat(algebra/module/polynomial): Modules over `R[X]` #14666

pbazin wants to merge 9 commits into master from module_over_polynomial

initial commit

308a4c7e

lint style

663129ff

lint + dedup

0686e284

eric-wieser commented on 2022-06-12

eric-wieser commented on 2022-06-13

use of_module

409c4468

eric-wieser added awaiting-author

eric-wieser removed awaiting-author

eric-wieser added awaiting-review

eric-wieser commented on 2022-06-29

simp

6d4d8ca2

kbuzzard approved these changes on 2022-07-18

blank ines

bcdd3798

ADedecker added t-algebra

jcommelin changed the title ~~feat(algebra/module/polynomial.lean): Modules over `R[X]`~~ feat(algebra/module/polynomial): Modules over `R[X]` 3 years ago

jcommelin requested a review from

erdOne 3 years ago

erdOne commented on 2022-08-15

erdOne removed awaiting-review

erdOne added awaiting-author

add momomial + is_scalar_tower

f0e73ea5

Merge branch 'master' into module_over_polynomial

fae75d5e

fix has_scalar to has_smul

92978f46

kim-em added too-late

Reviewers

kbuzzard

erdOne

eric-wieser

Assignees

No one assigned

Labels

awaiting-author t-algebra too-late

Milestone

No milestone

mathlib3 feat(algebra/module/polynomial): Modules over `R[X]` #14666 Open

feat(algebra/module/polynomial): Modules over `R[X]` #14666

mathlib3
feat(algebra/module/polynomial): Modules over `R[X]`
#14666

Open