leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 4 years ago

7a6ee0c4

feat(linear_algebra/unitary_group): add a group structure on unitary_submonoid

eric-wieser committed 4 years ago

9f85080e

refactor(analysis/complex/circle): The circle group is commutative (#11368)

tb65536 committed 4 years ago

de9944b1

refactor(logic/small, *): Infer `f : α → β` when followed by a simple condition on `f` (#11037)

vihdzp committed 4 years ago

e8839a30

feat(algebra/big_operators): add product versions of some sum lemmas (#11358)

alexjbest committed 4 years ago

89bff5e7

chore(simple_graph/basic): Fix typo in docstring: adjacent vertices, not edges (#11356)

nomeata committed 4 years ago

d8a75bd0

feat(ring_theory/discriminant): remove an assumption (#11359)

riccardobrasca committed 4 years ago

8910f6d9

feat(analysis/normed_space/linear_isometry): basis ext lemmas (#11331)

jsm28 committed 4 years ago

fd51bda5

feat(analysis/inner_product_space/basic): inner products of linear combinations of orthonormal vectors (#11323)

jsm28 committed 4 years ago

3b55b948

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

Older