leanprover-community/mathlib3

Pull Requests Commits

feat(algebraic_geometry): The function field is the fraction field of stalks (#11129)

erdOne committed 3 years ago

91a1afb4

feat(data/finsupp/interval): Finitely supported functions to a locally finite order are locally finite (#10930)

YaelDillies committed 3 years ago

0b6330de

fix(tactic/squeeze): `squeeze_simp` providing invalid suggestions (#11696)

arthurpaulino committed 3 years ago

445be96e

feat(data/list/*): subperm_singleton_iff (#11680)

ericrbg committed 3 years ago

3837abcb

feat(order/filter/countable_Inter): review (#11673)

urkud committed 3 years ago

1e44add0

feat(order/hom/basic): `compl` as a dual order isomorphism (#11630)

TwoFX committed 3 years ago

680733c3

feat(order/max): Predicate for minimal/maximal elements, typeclass for orders without bottoms (#11618)

YaelDillies committed 3 years ago

ff241e13

feat(category_theory/bicategory/natural_transformation): define oplax natural transformations (#11404)

yuma-mizuno committed 3 years ago

2fa59776

chore(order/locally_finite): fill in finset interval API (#11338)

b-mehta committed 3 years ago

b9db1696

feat(ring_theory/polynomial/eisenstein): add miscellaneous results about Eisenstein polynomials (#11697)

riccardobrasca committed 3 years ago

924aab15

feat(data/quot): add subsingleton instances (#11668)

nomeata committed 3 years ago

e290b29c

feat(algebraic_geometry): Fiber products of schemes (#10605)

erdOne committed 3 years ago

bf347f9c

feat(data/mv_polynomial/derivation): derivations of `mv_polynomial`s (#9145)

urkud committed 3 years ago

67dcdef2

feat(group_theory/sylow): `fintype (sylow p H)` from `fintype (sylow p G)` (#11664)

tb65536 committed 3 years ago

6687cf15

feat(topology/category/Compactum): forget creates limits (#11690)

adamtopaz committed 3 years ago

f5d63f9f

chore(set_theory/ordinal_arithmetic): Golf some instances of `lt_irrefl _ h` down to `h.false` (#11699)

vihdzp committed 3 years ago

24cfb883

chore(order/conditionally_complete_lattice): move code to a new file (#11698)

urkud committed 3 years ago

bac0f55e

feat(analysis/special_functions/log): log of natural power (#11685)

b-mehta committed 3 years ago

21cea47a

feat(order/succ_pred/relation): `succ`/`pred` inductions on relations (#11518)

fpvandoorn committed 3 years ago

79e6cb09

feat(data/nat): a predicate for prime powers (#11313)

b-mehta committed 3 years ago

0a721ccc

chore(set_theory/ordinal_arithmetic): golf proof into term mode (#11691)

vihdzp committed 3 years ago

74584760

doc(polynomial/eval): why map_ring_hom can't replace map (#11537)

ericrbg committed 3 years ago

02c08d9b

feat(archive/100-theorems-list): add proof of the solution of the cubic (#11635)

null-lambda committed 3 years ago

05e1845c

feat(set_theory/ordinal_arithmetic): Update header (#11681)

vihdzp committed 3 years ago

08445971

feat(set_theory/ordinal_arithmetic): Proved `sup_eq_lsub_iff_lt_sup` (#11660)

vihdzp committed 3 years ago

a6ace8c1

chore(analysis/complex/cauchy_integral): use `dslope` to golf a proof (#11675)

urkud committed 3 years ago

92ee748e

feat(order/filter): +1 version of `mem_inf_principal` (#11674)

urkud committed 3 years ago

a1e1ffd1

chore(*): don't use tactic internal lemmas in proofs (#11641)

alexjbest committed 3 years ago

52e9fd52

chore(topology/algebra/uniform_group): Remove newline after docstring (#11671)

tb65536 committed 3 years ago

577e3a22

feat(data/nat/factorization): various theorems on factorization and division (#11663)

stuart-presnell committed 3 years ago

946454a8

Newer Older