leanprover-community/mathlib

Pull Requests Commits

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

feat(archive/imo): formalize IMO 2011 problem Q3 (#5842)

dwrensha committed 4 years ago

1eb12937

feat(data/real/{nnreal,ennreal}, topology/instances/ennreal): add of_real_(sum/prod/tsum) for nnreal and ennreal (#5896)

RemyDegenne committed 4 years ago

531bcd8d

feat(data/finset/basic): card_subtype simp lemma (#5894)

pechersky committed 4 years ago

8c732b2c

feat(analysis/{analytic,calculus}): an analytic function is strictly differentiable (#5878)

urkud committed 4 years ago

547d67fc

chore(data/finset): Rename bind to bUnion (#5813)

kmill committed 4 years ago

44fd23d1

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

leanprover-community-bot committed 4 years ago

01a7cde6

feat(data/fintype/basic): add lemmas about finsets and cardinality (#5886)

agusakov committed 4 years ago

5491c592

chore(algebra/group_with_zero): correct instance name (#5885)

eric-wieser committed 4 years ago

7f25aa76

Newer Older