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