leanprover-community/mathlib3

Pull Requests Commits

feat(group_theory/abelianization): Add fintype instance (#11302)

tb65536 committed 4 years ago

fd524810

feat(analysis/inner_product_space/orientation): orientations of real inner product spaces (#11269)

jsm28 committed 4 years ago

2642c89b

feat(set_theory/ordinal_arithmetic): Enumerating unbounded sets of ordinals with ordinals (#10979)

vihdzp committed 4 years ago

4e7e5a6e

feat(algebra/associated): add lemmas to split #9345 (#10941)

Paul-Lez committed 4 years ago

8e92af1d

feat(data/finsupp/pointwise): add a definition of the pointwise action of functions on finsupps (#10933)

alexjbest committed 4 years ago

4bf48590

feat(data/set/basic): add decidable instances for boolean operations (#11354)

gebner committed 4 years ago

2e003c9a

feat(data/nat/factorization): Evaluating a multiplicative function over prime power divisors (#11167)

stuart-presnell committed 4 years ago

427e5b59

feat(data/polynomial/erase_lead): introduce two lemmas to compute `nat_degree`s under certain maps (#11265)

adomani committed 4 years ago

dc3cbb7d

feat(data/nat/cast): generalize to `fun_like` (#11128)

ericrbg committed 4 years ago

168ad7fc

feat(logic/basic): add eq_true_eq_id (#11341)

BoltonBailey committed 4 years ago

1533f158

feat(linear_algebra/determinant): `linear_equiv.det_conj` (#11340)

jsm28 committed 4 years ago

fabc5101

feat(probability_theory/martingale): one direction of the optional stopping theorem (#11007)

kex-y committed 4 years ago

48b21e51

feat (data/finset/lattice): add more finset induction lemmas (#10889)

MantasBaksys committed 4 years ago

77821571

chore(data/set/function): move inv_fun_on out of `logic/function/basic` (#11330)

eric-wieser committed 4 years ago

99fe7acb

fix(docs/references.bib): syntax error (#11342)

robertylewis committed 4 years ago

6a109397

feat(topology/algebra/monoid): to_additivize some lemmas (#11310)

alexjbest committed 4 years ago

ce17b657

chore(*): update to 3.37.0c (#11325)

ericrbg committed 4 years ago

d13b3a4a

refactor(data/{sigma,psigma}/order): Use `lex` synonym and new notation (#11235)

YaelDillies committed 4 years ago

47a8d5a6

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

Newer Older