leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 4 years ago

90cb2081

Revert dfinsupp changes

eric-wieser committed 4 years ago

e8a5d6a0

Partially fix mul_one

eric-wieser committed 4 years ago

5f8594d7

Merge remote-tracking branch 'origin/master' into eric-wieser/dadd_monoid_algebra

eric-wieser committed 4 years ago

fd0411df

refactor(category_theory/abelian): golf `mono_of_kernel_ι_eq_zero` (#5914)

Jesse Michael Han committed 4 years ago

e5f9409c

refactor(data/complex/exponential): simplify proof of `tan_eq_sin_div_cos` (#5913)

Jesse Michael Han committed 4 years ago

1688b3e8

refactor(data/holor): simp -> refl (#5912)

Jesse Michael Han committed 4 years ago

e927930c

refactor(algebra/category/Group/limits): simp -> refl (#5911)

Jesse Michael Han committed 4 years ago

38f6e050

refactor(data/real/golden_ratio): simpler proof of `gold_pos` (#5910)

Jesse Michael Han committed 4 years ago

6eae6303

refactor(data/pequiv): simpler proof of `pequiv.of_set_univ` (#5907)

Jesse Michael Han committed 4 years ago

e9a1e2b3

refactor(algebra/group/basic): simp -> rw in `sub_eq_sub_iff_sub_eq_sub` (#5903)

Jesse Michael Han committed 4 years ago

fd55e57f

chore(data/finset/preimage): add missing simp lemmas (#5902)

eric-wieser committed 4 years ago

1cd22862

chore(*): add more simp lemmas, refactor theorems about `fintype.sum` (#5888)

urkud committed 4 years ago

20d6b6a7

feat(algebra/euclidean_domain): Unify occurences of div_add_mod and mod_add_div (#5884)

Julian-Kuelshammer committed 4 years ago

21e9d424

refactor(ring_theory/ideal ring_theory/jacobson): allow `ideal` in a `comm_semiring` (#5879)

adomani committed 4 years ago

688772e9

feat(ring_theory/noetherian, linear_algebra/basic): Show that finitely generated submodules are the compact elements in the submodule lattice (#5871)

cemulate committed 4 years ago

b2c5d9b2

feat(field_theory/adjoin): Generalize alg_hom_mk_adjoin_splits to infinite sets (#5860)

tb65536 committed 4 years ago

7f04253c

feat(field_theory/normal): Restrict to normal subfield (#5845)

tb65536 committed 4 years ago

e95928c0

feat(linear_algebra/matrix): A vector is zero iff its dot product with every vector is zero (#5837)

kex-y committed 4 years ago

61491ca3

chore(data/finsupp,data/dfinsupp,algebra/big_operators): add missing lemmas about sums of bundled functions (#5834)

eric-wieser committed 4 years ago

31edca86

chore(category_theory/monad): comonadic adjunction (#5770)

b-mehta committed 4 years ago

aa8980d9

chore(data/fintype/basic): Add simp lemma about finset.univ (#5708)

eric-wieser committed 4 years ago

3b6d6d74

feat(data/polynomial/denominators): add file denominators (#5587)

adomani committed 4 years ago

00b88eb1

refactor(data/nat/factorial): simpler proof of `mul_factorial_pred` (#5917)

Jesse Michael Han committed 4 years ago

394d3574

refactor(topology/metric_space): simplify `dist_triangle` proofs (#5916)

Jesse Michael Han committed 4 years ago

d41781cf

chore(*): split long lines (#5908)

urkud committed 4 years ago

4e4298e2

chore(*): Replace integral_domain assumptions with no_zero_divisors (#5877)

eric-wieser committed 4 years ago

47e2f804

chore(scripts): update nolints.txt (#5918)

leanprover-community-bot committed 4 years ago

19bb4709

chore(tactic/finish): Remove broken ifinish (#5897)

PatrickMassot committed 4 years ago

91730057

feat(analysis/normed_space): define linear isometries (#5867)

urkud committed 4 years ago

1ddb93a9

Older