leanprover-community/mathlib3

Pull Requests Commits

chore(data/complex/basic): upgrade `complex.norm_sq` to a `monoid_with_zero_hom` (#5553)

urkud committed 5 years ago

9f6300e9

feat(ring_theory/simple_module): simple modules and Schur's Lemma (#5473)

awainverse committed 5 years ago

9d3c05ad

feat(algebra/ordered_group): add linear_ordered_comm_group and linear_ordered_cancel_comm_monoid (#5286)

kbuzzard committed 5 years ago

afc3f03a

chore(data/list): a list sorted w.r.t. `(<)` has no duplicates (#5550)

urkud committed 5 years ago

d94f0a27

chore(algebra/*): move some lemmas to `div_inv_monoid` (#5552)

urkud committed 5 years ago

409ea425

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

urkud committed 5 years ago

06a11fd5

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

hrmacbeth committed 5 years ago

ea3815fb

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

kbuzzard committed 5 years ago

b57d562c

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

urkud committed 5 years ago

c32efeae

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

urkud committed 5 years ago

8aa23326

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

urkud committed 5 years ago

e0030ffe

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

hrmacbeth committed 5 years ago

b542cfbc

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

fpvandoorn committed 5 years ago

fcbaf625

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

leanprover-community-bot committed 5 years ago

d2bde119

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

pechersky committed 5 years ago

54bf708d

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

urkud committed 5 years ago

0830bfd4

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

hrmacbeth committed 5 years ago

10f6c151

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

tb65536 committed 5 years ago

cca63650

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

kckennylau committed 5 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

Newer Older