leanprover-community/mathlib3

Pull Requests Commits

chore(linear_algebra/basis): split off `linear_independent.lean` (#4440)

Vierkantor committed 5 years ago

21271659

feat(order/filter/ultrafilter): Add variant of `exists_ultrafilter`. (#4436)

adamtopaz committed 5 years ago

88c76ab9

lint(order/conditionally_complete_lattice): docstrings (#4434)

hrmacbeth committed 5 years ago

91515320

feat(ring_theory/ideal): ideals in product rings (#4431)

TwoFX committed 5 years ago

221ec606

lint(category_theory/whiskering): add doc-strings (#4417)

kim-em committed 5 years ago

f9e3779b

feat(algebra/gcd_monoid): `gcd_mul_dvd_mul_gcd` (#4386)

awainverse committed 5 years ago

d2140efb

docs(tactic/{fin_cases,lift}): lint (#4421)

robertylewis committed 5 years ago

c58c4e62

chore(*/multilinear): generalize `comp_linear_map` to a family of linear maps (#4408)

urkud committed 5 years ago

e89d0edd

feat(data/mv_polynomial/basic): map_map_range_eq_iff (#4438)

jcommelin committed 5 years ago

7f74e6b3

feat(data/rat/basic): denom_eq_one_iff (#4437)

jcommelin committed 5 years ago

39f5d6b6

chore(src/linear_algebra): linting (#4427)

Vierkantor committed 5 years ago

22398f3e

feat(linear_algebra/affine_space/finite_dimensional): collinearity (#4433)

jsm28 committed 5 years ago

ca269b44

chore(category_theory/yoneda): doc-strings (#4429)

kim-em committed 5 years ago

b0fe280b

chore(data/fin2): linting (#4426)

kmill committed 5 years ago

1501bf6f

chore(linear_algebra/finsupp*): linting (#4425)

Vierkantor committed 5 years ago

dd73dd2a

chore(data/fintype/basic): linting (#4424)

kmill committed 5 years ago

c058524c

data(data/dlist/{basic,instances}): linting (#4422)

kmill committed 5 years ago

70b8e828

chore(data/buffer/basic): linting (#4420)

kmill committed 5 years ago

da1265c5

chore(data/array/lemmas): linting (#4419)

kmill committed 5 years ago

768ff768

chore(data/W): linting (#4418)

kmill committed 5 years ago

c370bd06

lint(category_theory/adjunction): add doc-strings (#4415)

kim-em committed 5 years ago

6a4fd24a

chore(algebra/direct_sum): linting (#4412)

jcommelin committed 5 years ago

17b607f7

feat(data/finsupp): Make `finsupp.dom_congr` a `≃+` (#4398)

eric-wieser committed 5 years ago

b44e927e

chore(algebra/group/with_one): prove `group_with_zero` earlier, drop custom lemmas (#4385)

urkud committed 5 years ago

54a2c6b6

refactor(linear_algebra/matrix): consistent naming (#4345)

Vierkantor committed 5 years ago

72360845

chore(logic/relation): linting (#4414)

kmill committed 5 years ago

67b312c2

feat(*): assorted `simp` lemmas for IMO 2019 q1 (#4383)

urkud committed 5 years ago

186660c0

feat(combinatorics/partitions): Add partitions (#4303)

b-mehta committed 5 years ago

8f4475b4

chore(algebra/direct_limit): linting (#4411)

jcommelin committed 5 years ago

ca679aca

feat(data/complex): norm_cast lemmas (#4405)

jsm28 committed 5 years ago

581b1415

Newer Older