leanprover-community/mathlib3

Pull Requests Commits

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

feat(data/set/finite): add to_finset lemma (#5883)

agusakov committed 4 years ago

3a16e9f8

feat(data/set/finite): add lemma about to_finset of complement of set (#5881)

agusakov committed 4 years ago

ba876475

chore(algebra/pi_tensor_product): Replace use of classical with decidable_eq (#5880)

eric-wieser committed 4 years ago

7188d806

feat(analysis/normed_space/inner_product): double orthogonal complement is closure (#5876)

hrmacbeth committed 4 years ago

1dfa81a1

chore(algebra): a few more `@[mono]` tags (#5874)

urkud committed 4 years ago

ee750e33

feat(measure_theory/{measure_space, borel_space, integration}): prove ae_measurable for various limits (#5849)

RemyDegenne committed 4 years ago

6d806348

chore(archive/sensitivity): split long lines (#5882)

urkud committed 4 years ago

d6d4435e

feat(order/atoms): define (co)atomic, (co)atomistic lattices (#5588)

awainverse committed 4 years ago

9117ad71

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

leanprover-community-bot committed 4 years ago

87202fe9

Newer Older