leanprover-community/mathlib3

Pull Requests Commits

Generalize the universe variable

eric-wieser committed 4 years ago

b58c3c09

feat(data/fintype/basic): add decidable_eq_(bundled-hom)_fintype (#7394)

eric-wieser committed 4 years ago

c50cb7a7

feat(linear_algebra/free_module): free of finite torsion free (#7381)

PatrickMassot committed 4 years ago

abf1c205

chore(*): use `sq` as convention for "squared" (#7368)

benjamindavidson committed 4 years ago

b9c80c92

feat(group_theory/finiteness): add group.fg (#7338)

riccardobrasca committed 4 years ago

2401d996

feat(topology/continuous_function): abstract statement of Weierstrass approximation (#7303)

kim-em committed 4 years ago

4328cc3c

chore(algebra/module/submodule): mem_to_add_subgroup (#7392)

jcommelin committed 4 years ago

e6a4c818

feat(algebra/group/hom_instance): add add_monoid_hom.mul (#7382)

eric-wieser committed 4 years ago

052447d3

feat(algbera/lie/submodule): add `simp` lemmas `lie_submodule.map_sup`, `lie_ideal.map_sup` (#7384)

ocfnash committed 4 years ago

a1b695af

feat(linear_algebra/finite_dimensional): characterizations of finrank = 1 and ≤ 1 (#7354)

kim-em committed 4 years ago

105935c0

refactor(algebra/big_operators/finprod, ring_theory/hahn_series): summable families now use `finsum` (#7388)

awainverse committed 4 years ago

f952dd11

chore(.): remove stray file (#7390)

kim-em committed 4 years ago

db890829

fix(algebra/group/commute): use the right typeclass (#7389)

eric-wieser committed 4 years ago

97118b45

feat(logic/embedding): add function.embedding.coe_injective (#7383)

eric-wieser committed 4 years ago

d40a60c8

fix(tactic/itauto): reset after or split (#7387)

digama0 committed 4 years ago

c562cafa

chore(.docker): fix alpine docker build (#7374)

kim-em committed 4 years ago

a24d4809

feat(analysis/analytic): a few lemmas about summability and radius (#7365)

ADedecker committed 4 years ago

1ff56a03

feat(algebra/group_with_zero): add semigroup_with_zero (#7346)

eric-wieser committed 4 years ago

5247d00f

feat(data/buffer/parser/basic): nat_eq_done (#6340)

pechersky committed 4 years ago

78a20ffc

chore(algebra/lie/{abelian,tensor_product}): rename `maximal_trivial_submodule` → `max_triv_submodule` (#7385)

ocfnash committed 4 years ago

5263ea32

docs(overview): Add some recent work by Yury (#7378)

PatrickMassot committed 4 years ago

e7bd3caa

feat(analysis/special_functions/integrals): integral of `sin x ^ n` (#7372)

benjamindavidson committed 4 years ago

efeeacaf

feat(topology/separation): change regular_space definition, added t1_characterisation and definition of Urysohn space (#7367)

carloscaralps committed 4 years ago

18403ac8

refactor(ring_theory/hahn_series): non-linearly-ordered Hahn series (#7377)

awainverse committed 4 years ago

287492c6

chore(integration): missing lemmas (#7364)

PatrickMassot committed 4 years ago

57cc3843

feat(analysis/seminorm): lemmas on balanced sets (#7358)

b-mehta committed 4 years ago

241400f8

feat(algebra/opposite): inversion is a mul_equiv to the opposite group (#7330)

eric-wieser committed 4 years ago

20c520a6

feat(category_theory/abelian): biproducts of projective objects are projective (#7319)

kim-em committed 4 years ago

465cf5ad

feat(data/quot): rec_on_subsingleton2' (#7294)

pechersky committed 4 years ago

874780fc

feat(analysis/calculus/deriv): `has_deriv_at.continuous_on` (#7260)

benjamindavidson committed 4 years ago

a3f589c0

Older