mathlib3
feat(proj construction)
#18138
Open

feat(proj construction) #18138

jjaassoonn wants to merge 62 commits into master from jjaassoonn/proj_rest
jjaassoonn
jjaassoonn initial
2fb86212
jjaassoonn add algebra instance
a2d09244
jjaassoonn linter
aa743774
jjaassoonn not finished
03fc97a9
jjaassoonn almost finished
a27c73f9
jjaassoonn finish
10947c6c
jjaassoonn shorten
61872f8f
jjaassoonn `carrier_eq_carrier'`
860fc49c
jjaassoonn first golf
81399fef
jjaassoonn reverse direction
fd2e8db0
jjaassoonn Merge remote-tracking branch 'origin/master' into jjaassoonn/proj_spe…
ce0bf44d
jjaassoonn mimize diff
7b45867d
jjaassoonn fix
5ffedfd7
jjaassoonn fix
b2461c2f
jjaassoonn fix long line
7768f9c5
jjaassoonn fix
8913a9a4
jjaassoonn fix
5dd54964
jjaassoonn fix lint error
c9bd0b75
jjaassoonn Update src/algebraic_geometry/projective_spectrum/scheme.lean
5218dc90
jjaassoonn Merge remote-tracking branch 'origin/master' into jjaassoonn/proj_spe…
868f5ed6
jjaassoonn partial fix `to_Spec_from_Spec`
34e48cb1
jjaassoonn fix `from_Spec`
cd163586
jjaassoonn fix namespace mismatch
093e7b50
jjaassoonn fix `data.num,.denom, num, denom, bmk_one`
0da52122
jjaassoonn fix `bmk_zero`
44ea7ee7
jjaassoonn fix `bmk_add`
efe52198
jjaassoonn clean useless comment
f165d495
jjaassoonn fix `bmk_mul`
3d9f09ab
jjaassoonn fix `Uo`
61437a32
jjaassoonn fix `subset2`
2e90f27e
jjaassoonn fix `is_locally_quotient`
a556fcc4
jjaassoonn fix `Proj_iso_Spec_Sheaf_component.from_Spec`
05438078
jjaassoonn add `to_Spec`, fix some trivial things
6f8ee013
jjaassoonn fix `fmk.one`
e211462a
jjaassoonn fix `fmk.one`
e033354c
jjaassoonn fix `fmk.add`
10f2a6fd
jjaassoonn fix `fmk.mul`
8e1c5565
jjaassoonn fix `not_mem`
014309ef
jjaassoonn fix `final_eq`
565668d2
jjaassoonn fix `inv_hom_mem_bo`, `inv_hom_mem2`
c3356018
jjaassoonn fix `fmk_is_locally_quotient`
eb1a98e3
jjaassoonn fix `Proj_iso_Spec_Sheaf_component.to_Spec`
4893f6fb
jjaassoonn fix preliminary lemmas for `from_Spec_to_Spec`
2b279d03
jjaassoonn fix `from_Spec_to_Spec`
c79ffb75
jjaassoonn fix `to_Spec_from_Spec`
216fe782
jjaassoonn fix everything
9ee848ad
jjaassoonn Merge remote-tracking branch 'origin/master' into jjaassoonn/proj_rest
bd4f437f
jjaassoonn fix import
3b8d1b70
jjaassoonn a bunch of comment
8e2c876b
jjaassoonn finished documenting
72d5d6bd
jjaassoonn argument linter fix
a344a69d
jjaassoonn changed long lines and another unused argument error
d57075d8
jjaassoonn fix build error
dfedbe84
jjaassoonn fix many linter long line and golf many proofs
b6647422
jjaassoonn this should fix all linter error, perhaps,probably
f8f59c33
jjaassoonn this should fix all linter error, perhaps,probably
c93f889a
jjaassoonn fix timeout
94024314
jjaassoonn complete documentation at header
08177de6
jjaassoonn add projectve space
df1a8ba4
jjaassoonn fix linter
5b506dda
jjaassoonn add doc
de2f88fc
jjaassoonn fix long line
00c4b091
kim-em
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
Milestone