leanprover-community/mathlib3

Pull Requests Commits

feat(algebra/periodic): lifting to function on quotient group (#11321)

jsm28 committed 4 years ago

2bb25f05

feat(vscode): add a snippet for inserting a module docstring template (#11312)

alexjbest committed 4 years ago

49ba33e5

feat(field_theory/ratfunc): ratfunc.lift_on without is_domain (#11227)

pechersky committed 4 years ago

fadbd959

split(data/set/functor): Split off `data.set.lattice` (#11327)

YaelDillies committed 4 years ago

9c224ff6

chore(*): miscellaneous to_additive related cleanup (#11316)

alexjbest committed 4 years ago

ad4ea538

feat(linear_algebra/basis): `basis.ext`, `basis.ext'` for semilinear maps (#11317)

jsm28 committed 4 years ago

ca5e55cc

feat(data/nat/factorization): Add lemmas on factorizations of pairs of coprime numbers (#10850)

stuart-presnell committed 4 years ago

a58553d5

chore(ring_theory/fractional_ideal): fix typo (#11311)

ericrbg committed 4 years ago

d4846b32

feat(combinatorics/simple_graph/matchings): even_card_vertices_of_perfect_matching (#11083)

arthurpaulino committed 4 years ago

22ff4ebc

feat(linear_algebra/eigenspace): prove eigenvalues are exactly elements of the spectrum when the space is finite dimensional (#10961)

j-loreaux committed 4 years ago

0a75fdfb

chore(set_theory/game/domineering): extract repeated goal into lemma and golf (#11298)

eric-wieser committed 4 years ago

ee136d90

feat(topology/basic): add explicit definition of continuous_at (#11296)

fpvandoorn committed 4 years ago

84dbe31d

docs(algebra/covariant_and_contravariant): minor typos (#11293)

robertylewis committed 4 years ago

25704cac

chore(analysis/normed_space/banach): move more to the `continuous_linear_map` NS (#11263)

urkud committed 4 years ago

09f69890

chore(*): update to lean 3.36.0 (#11253)

ericrbg committed 4 years ago

60e279ba

feat(algebra/associated): generalize nat.prime.pow_dvd_of_dvd_mul_{left,right} (#11301)

Ruben-VandeVelde committed 4 years ago

dd1242d2

feat(ring_theory/laurent): coercion of R[x] to R((x)) lemmas (#11295)

pechersky committed 4 years ago

c76e1136

chore(data/fin/vec_notation): generalize smul_cons (#11285)

eric-wieser committed 4 years ago

11625097

feat(data/polynomial/{erase_lead + denoms_clearable}): strengthen a lemma (#11257)

adomani committed 4 years ago

56f021a9

refactor(combinatorics/quiver): split into several files (#11006)

dwarn committed 4 years ago

b181a120

feat(algebraic_geometry): Gamma-Spec adjunction (#9802)

alreadydone committed 4 years ago

9b3fec55

feat(data/matrix/basic): infix notation for matrix.dot_product in locale matrix (#11289)

madvorak committed 4 years ago

b1955dca

feat(ring_theory/power_series): teach simp to simplify more coercions of polynomials to power series (#11287)

alexjbest committed 4 years ago

43041277

feat(number_theory/cyclotomic/basic): add lemmas (#11264)

riccardobrasca committed 4 years ago

e8713864

feat(data/nat/prime): power to factor count divides natural (#11226)

b-mehta committed 4 years ago

c7fa66ea

chore(measure_theory/group/arithmetic): use implicit argument for measurable_space (#11205)

RemyDegenne committed 4 years ago

4d79d5fe

feat(group_theory/commuting_probability): New file (#11243)

tb65536 committed 4 years ago

22311732

feat(data/sum/order): Linear and disjoint sums of orders (#11157)

YaelDillies committed 4 years ago

07f9b8e1

feat(topology/metric_space/hausdorff_distance): make iffs (#11288)

fpvandoorn committed 4 years ago

303e77c8

feat(data/finset/sym): Symmetric powers of a finset (#11142)

YaelDillies committed 4 years ago

5cbfddd3

Older