leanprover-community/mathlib3

Pull Requests Commits

merged the two halves

jakelev committed 3 years ago

f98685a9

second half of stalk surjectivity lemma

jakelev committed 3 years ago

4453f2fd

one direction of the proof

samvang committed 3 years ago

f6be8e05

defined surjectivity on stalks

jakelev committed 3 years ago

2a2112a2

some cleanup and notation

samvang committed 3 years ago

3f0fc6bc

still more brainstorming

jakelev committed 3 years ago

c0736c32

some brainstorming on open subschemes

jakelev committed 3 years ago

d1df8f5e

notation is mostly set up

jakelev committed 3 years ago

b51c0c68

a definition of locally surjective and closed immersion

samvang committed 3 years ago

7f99f5e1

a few more edits

jakelev committed 3 years ago

58853331

defined is_locally_surjective

jakelev committed 3 years ago

fffe1497

first stub of closed immersion for schemes

samvang committed 3 years ago

07b43747

renaming to make file compile

samvang committed 3 years ago

387d8dcf

add our work from PR #15291

samvang committed 3 years ago

ef22abf0

chore(analysis/inner_product_space): move definition of self-adjointness (#15281)

mcdoll committed 3 years ago

1d048c57

feat(ring_theory/rees_algebra): Define the Rees algebra of an ideal. (#15089)

erdOne committed 3 years ago

2dfa69c1

feat(measure_theory/pmf): lawful monad instance for probability mass function monad (#15066)

dtumad committed 3 years ago

8d7f0012

feat(data/matrix/notation): add `!![1, 2; 3, 4]` notation (#14991)

eric-wieser committed 3 years ago

83092fb4

feat(data/polynomial/unit_trinomial): An irreducibility criterion for unit trinomials (#14914)

tb65536 committed 3 years ago

01a18244

feat(data/polynomial/erase_lead): Characterization of polynomials of fixed support (#14741)

tb65536 committed 3 years ago

581b6940

feat(information_theory/hamming): add Hamming distance and norm (#14739)

linesthatinterlace committed 3 years ago

73402033

chore(scripts): update nolints.txt (#15293)

leanprover-community-bot committed 3 years ago

b06e32c2

refactor(logic/is_empty): tag `is_empty.forall_iff` and `is_empty.exists_iff` as `simp` (#14660)

vihdzp committed 3 years ago

5cb17dd1

refactor(topology/subset_properties): reformulate `is_clopen_b{Union,Inter}` in terms of `set.finite` (#15272)

urkud committed 3 years ago

ea13c1cf

feat(data/finsupp/basic): graph of a finitely supported function (#15197)

vihdzp committed 3 years ago

2a325960

feat(algebra/parity): more general odd.pos (#15186)

ericrbg committed 3 years ago

c6014bd2

refactor(topology/separation): rename `regular_space` to `t3_space` (#15169)

urkud committed 3 years ago

ede73b25

refactor(data/matrix/basic): add matrix.of for type casting (#14992)

eric-wieser committed 3 years ago

6c351a8f

feat(topology/maps): more `iff` lemmas (#15165)

urkud committed 3 years ago

834488ee

feat(analysis/special_functions/pow): drop an assumption in `is_o_log_rpow_rpow_at_top` (#15164)

urkud committed 3 years ago

7bd47556

Older