mathlib3
feat(data/power_series): Add multivariate power series and prove basic API
#1244
Merged
Merged
feat(data/power_series): Add multivariate power series and prove basic API #1244
mergify
merged
46 commits into
master
from
power-series
First start on power_series
12acd3c0
Innocent changes
8b7eb311
Almost a comm_semiring
146405a0
Defined hom from mv_polynomial to mv_power_series; sorrys remain
0f01f4ab
Attempt that seem to go nowhere
eaa538ac
Working on coeff_mul for polynomials
2bc7b647
Small progress
d26b9390
Finish mv_polynomial.coeff_mul
bfde6d7e
Cleaner proof of mv_polynomial.coeff_mul
907584d4
Fix build
be0b909a
WIP
d4b3672a
Finish proof of mul_assoc
0afb898b
WIP
9f3160a8
Merge branch 'lean-3.4.2' into power-series
99dd853b
Golfing coeff_mul
4ee9f0cc
WIP
dac14700
Crazy wf is crazy
81195b14
mv_power_series over local ring is local
faf92d87
WIP
7a18a281
Add empty line
3bba2bf8
wip
10169aa5
wip
f30a689f
WIP
aeae8ae7
WIP
a1c7cb5a
WIP
be25bd87
Add header comments
a3d76909
WIP
70744fb9
WIP
332840d7
Merge branch 'lean-3.4.2' into power-series
095a6886
Fix finsupp build
21b465b6
Fix build, hopefully
7b8ef4ca
Fix build: ideals
355e72f4
More docs
3ad952e6
jcommelin
commented
on 2019-07-20
Update src/data/power_series.lean
2ed1f929
Fix build -- bump instance search depth
d19b653d
Merge branch 'power-series' of github.com:leanprover-community/mathli…
ed960c0a
Make changes according to some of the review comments
534ddb8f
Use 'formal' in the names
340a4d24
Use 'protected' in more places, remove '@simp's
006debaf
Make 'inv_eq_zero' an iff
e8479040
Generalize to non-commutative scalars
9a58c5f2
Move file
f6814982
Undo name change, back to 'power_series'
b3c5f468
ChrisHughes24
commented
on 2019-07-22
spelling mistake
a85bce8b
ChrisHughes24
commented
on 2019-07-22
spelling mistake
80f283f4
ChrisHughes24
approved these changes
on 2019-07-22
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into power-series
de39b926
Login to write a write a comment.
Login via GitHub