leanprover-community/mathlib3

Pull Requests Commits

awainverse committed 4 years ago

2ada12f7

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

feat(data/polynomial): lemma about aeval on functions, and on subalgebras (#7252)

kim-em committed 4 years ago

4f9543bb

feat(category/subobjects): more API on limit subobjects (#7203)

kim-em committed 4 years ago

89c27ccd

feat(algebra/direct_sum): state what it means for a direct sum to be internal (#7190)

eric-wieser committed 4 years ago

40b15f25

chore(group_theory/eckmann_hilton): use `mul_one_class` and `is_(left|right)_id` (#7370)

eric-wieser committed 4 years ago

2d8ed1f5

refactor(archive/imo) shorten imo1013_q5 using pow_unbounded_of_one_lt (#7373)

dwrensha committed 4 years ago

17424431

chore(algebra/category/*): use by apply to speed up elaboration (#7360)

kim-em committed 4 years ago

3093fd81

feat(order/zorn): upward inclusion variant of Zorn's lemma (#7362)

YaelDillies committed 4 years ago

a5cb13a6

Older