leanprover-community/mathlib3

Pull Requests Commits

jjaassoonn committed 2 years ago

00c4b091

jjaassoonn committed 2 years ago

de2f88fc

jjaassoonn committed 2 years ago

5b506dda

add projectve space

jjaassoonn committed 2 years ago

df1a8ba4

complete documentation at header

jjaassoonn committed 2 years ago

08177de6

jjaassoonn committed 2 years ago

94024314

this should fix all linter error, perhaps,probably

jjaassoonn committed 2 years ago

c93f889a

this should fix all linter error, perhaps,probably

jjaassoonn committed 2 years ago

f8f59c33

fix many linter long line and golf many proofs

jjaassoonn committed 2 years ago

b6647422

fix build error

jjaassoonn committed 2 years ago

dfedbe84

changed long lines and another unused argument error

jjaassoonn committed 2 years ago

d57075d8

argument linter fix

jjaassoonn committed 2 years ago

a344a69d

finished documenting

jjaassoonn committed 2 years ago

72d5d6bd

a bunch of comment

jjaassoonn committed 2 years ago

8e2c876b

jjaassoonn committed 2 years ago

3b8d1b70

Merge remote-tracking branch 'origin/master' into jjaassoonn/proj_rest

jjaassoonn committed 2 years ago

bd4f437f

fix(tactic/{norm_num, abel}): do not do syntactic matches on typeclass instances (#18129)

eric-wieser committed 2 years ago

ec322deb

feat(topology/instances/ennreal): curried version of `ennreal.tsum_prod` (#18124)

dtumad committed 2 years ago

f8355031

feat(group_theory/group_action/support): Support under an action (#17055)

YaelDillies committed 2 years ago

36a35211

jjaassoonn committed 2 years ago

9ee848ad

fix `to_Spec_from_Spec`

jjaassoonn committed 2 years ago

216fe782

fix `from_Spec_to_Spec`

jjaassoonn committed 2 years ago

c79ffb75

fix preliminary lemmas for `from_Spec_to_Spec`

jjaassoonn committed 2 years ago

2b279d03

fix `Proj_iso_Spec_Sheaf_component.to_Spec`

jjaassoonn committed 2 years ago

4893f6fb

fix `fmk_is_locally_quotient`

jjaassoonn committed 2 years ago

eb1a98e3

refactor(linear_algebra/tensor_product): make `lift f (x ⊗ₜ y) = f x y` true by `rfl` (#18121)

eric-wieser committed 2 years ago

657df433

feat(analysis/special_functions): Gaussian integral with complex parameter (#18090)

loefflerd committed 2 years ago

914cb177

fix `inv_hom_mem_bo`, `inv_hom_mem2`

jjaassoonn committed 2 years ago

c3356018

jjaassoonn committed 2 years ago

565668d2

jjaassoonn committed 2 years ago

014309ef

Older