leanprover-community/mathlib3

Pull Requests Commits

chore(data/fintype/card): generalize `equiv.prod_comp` to `function.bijective.prod_comp` (#5551)

urkud committed 4 years ago

06a11fd5

feat(analysis/normed_space/inner_product): upgrade orthogonal projection to a continuous linear map (#5543)

hrmacbeth committed 4 years ago

ea3815fb

feat(algebra/big_operators/nat_antidiagonal): add prod_antidiagonal_eq_prod_range_succ (#5528)

kbuzzard committed 4 years ago

b57d562c

feat(data/fin): there is at most one `order_iso` from `fin n` to `α` (#5499)

urkud committed 4 years ago

c32efeae

chore(*): golf some proofs (#5548)

urkud committed 4 years ago

8aa23326

chore(data/real/cau_seq): golf some proofs (#5545)

urkud committed 4 years ago

e0030ffe

chore(linear_algebra/basic): notation for span of a singleton (#5538)

hrmacbeth committed 4 years ago

b542cfbc

doc(lint/type_classes): add has_coe_to_fun linter (#5546)

fpvandoorn committed 4 years ago

fcbaf625

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

leanprover-community-bot committed 4 years ago

d2bde119

feat(logic/basic): exists_unique_false simp lemma (#5544)

pechersky committed 4 years ago

54bf708d

refactor(analysis/analytic/basic): redefine `formal_multilinear_series.radius` (#5349)

urkud committed 4 years ago

0830bfd4

chore(analysis/normed_space/inner_product): notation for orthogonal complement (#5536)

hrmacbeth committed 4 years ago

10f6c151

feat(field_theory/galois): is_galois.tfae (#5542)

tb65536 committed 4 years ago

cca63650

chore(algebra): move lemmas from ring_theory.algebra_tower to algebra.algebra.tower (#5506)

kckennylau committed 4 years ago

b04aeb5e

feat(data/tprod): finite products of types (#5385)

fpvandoorn committed 5 years ago

a40f31fb

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

leanprover-community-bot committed 5 years ago

611b73eb

feat(field_theory/algebraic_closure): algebraically closed fields have no nontrivial algebraic extensions (#5537)

dtumad committed 5 years ago

9c46cadc

chore(algebra/field): use `K` as a type variable (#5535)

urkud committed 5 years ago

6e0d0fa4

feat(measure_theory): various additions (#5389)

fpvandoorn committed 5 years ago

99881936

feat(order/lattice_intervals): lattice structures on intervals in lattices (#5496)

awainverse committed 5 years ago

f1d2bc60

chore(topology/algebra/infinite_sum): refactor `tsum_mul_left/right` (#5533)

urkud committed 5 years ago

16320e2e

chore(analysis/normed_space/basic): a few lemmas about `nnnorm` (#5532)

urkud committed 5 years ago

958c407a

feat(topology/instances/ennreal): a sufficient condition for `f : (Σ i, β i) → ℝ` to be summable (#5531)

urkud committed 5 years ago

b15bb06e

chore(data/real/{e,}nnreal): a few lemmas (#5530)

urkud committed 5 years ago

38ba6ba2

feat(analysis/normed_space/inner_product): orthogonal complement lemmas (#5474)

hrmacbeth committed 5 years ago

c82be35d

chore(order/rel_iso): add some missing lemmas (#5492)

urkud committed 5 years ago

7a031718

chore(topology/algebra/ordered): move code, add missing lemmas (#5481)

urkud committed 5 years ago

8545aa60

chore(data/nat/enat): some useful lemmas (#5517)

jcommelin committed 5 years ago

5e86589d

fix(tactic/linarith): elaborate and insert arguments before destructing hypotheses (#5501)

robertylewis committed 5 years ago

1c110ada

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

leanprover-community-bot committed 5 years ago

7c6020f1

Newer Older