leanprover-community/mathlib

Pull Requests Commits

refactor(algebra/group_power): put lemmas about order and power in their own file (#7398)

eric-wieser committed 4 years ago

aebe7552

refactor(linear_algebra/eigenspace): cleanup proof (#7337)

kim-em committed 4 years ago

6d5a120f

feat(category_theory/Quiv): the free/forgetful adjunction between Cat and Quiv (#7158)

kim-em committed 4 years ago

5800f69a

feat(category_theory/sites): construct a presieve from an indexed family of arrows (#7413)

b-mehta committed 4 years ago

64fdfc74

feat(ring_theory/finiteness): add add_monoid_algebra.ft_of_fg (#7265)

riccardobrasca committed 4 years ago

4722dd46

feat(category_theory/sites): Sheaves of structures (#5927)

b-mehta committed 4 years ago

4a94b28f

chore(topology/category): some lemmas for Profinite functions (#7414)

b-mehta committed 4 years ago

f36cc164

refactor(data/fin): define neg like sub (#7408)

gebner committed 4 years ago

c914e8f5

feat(group/hom_instances): add composition operators (#7407)

eric-wieser committed 4 years ago

39a1cf0b

feat(finset/basic): fill in holes in the finset API (#7386)

YaelDillies committed 4 years ago

413b4263

refactor(algebraic_geometry/structure_sheaf): Remove redundant isomorphism (#7410)

justus-springer committed 4 years ago

6a796d08

feat(linear_algebra/tensor_product): add definition `tensor_product.map_incl` and `simp` lemmas related to powers of `tensor_product.map` (#7406)

ocfnash committed 4 years ago

ca5176c3

feat(set_theory/{surreal, pgame}): `mul_comm` for surreal numbers (#7376)

apurvnakade committed 4 years ago

966b3b18

chore(.docker): remove alpine build, too fragile (#7401)

kim-em committed 4 years ago

c9563537

feat(data/finsupp/to_dfinsupp): add equivalences between finsupp and dfinsupp (#7311)

eric-wieser committed 4 years ago

91604cbe

feat(data/rat): add `@[simp]` to `rat.num_div_denom` (#7393)

Vierkantor committed 4 years ago

fda4d3d5

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

Newer Older