leanprover-community/mathlib

Pull Requests Commits

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

feat(algebra/lie/tensor_product): prove `lie_submodule.lie_ideal_oper_eq_tensor_map_range` (#7313)

ocfnash committed 4 years ago

5ac79a63

feat(group_theory/finiteness): add submonoid.fg (#7279)

riccardobrasca committed 4 years ago

35b9d9c4

feat(topology/unit_interval): affine homeomorphisms of intervals (#7250)

kim-em committed 4 years ago

5258669e

chore(algebra/lie/nilpotent): make proof of `module.derived_series_le_lower_central_series` less refl-heavy (#7359)

ocfnash committed 4 years ago

c22de3f5

feat(data/nat/fib): add a strict monotonicity lemma. (#7317)

Julian committed 4 years ago

95260613

chore(analysis/special_functions/integrals): reorganize file (#7351)

benjamindavidson committed 4 years ago

4e0c460a

feat(data/matrix/basic): transform vec_mul to mul_vec (#7348)

gabrielmoise committed 4 years ago

dbc9cf9f

chore(ring_theory/ideal/operations): golf and remove @ (#7347)

eric-wieser committed 4 years ago

d5cb4033

Newer Older