leanprover-community/mathlib3

Pull Requests Commits

feat(algebra/polynomial/big_operators): coeff of sums and prods of polynomials (#8680)

pechersky committed 4 years ago

c4cf4c25

feat(ring_theory/trace): the trace form is nondegenerate (#8777)

Vierkantor committed 4 years ago

dcd60e25

feat(analysis/complex/isometry): Show that certain complex isometries are not equal (#8646)

shadasali committed 4 years ago

7f256987

feat(measure_theory/decomposition/radon_nikodym): the Radon-Nikodym theorem (#8763)

kex-y committed 4 years ago

7cfc9872

feat(algebra): define a bundled type of absolute values (#8881)

Vierkantor committed 4 years ago

023a816d

feat(ring_theory): a typeclass `is_integral_closure` (#8882)

Vierkantor committed 4 years ago

a3278519

feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib_aux (#8681)

pechersky committed 4 years ago

88e47d7c

refactor(*): use `is_empty` instead of `not (nonempty α)` (#8858)

urkud committed 4 years ago

0c503262

feat(category_theory/structured_arrow): Duality between structured and costructured arrows (#8807)

justus-springer committed 4 years ago

fe13f030

doc(ring_theory/hahn_series): Update Hahn Series docstring (#8883)

awainverse committed 4 years ago

4705a6b5

feat(algebra/big_operators/basic): add `prod_dite_of_false`, `prod_dite_of_true` (#8865)

ocfnash committed 4 years ago

a9de1979

feat(algebra/pointwise): add to_additive attributes for pointwise smul (#8878)

alexjbest committed 4 years ago

bcd5cd37

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

leanprover-community-bot committed 4 years ago

bb4026f4

feat(algebra/ordered_monoid): min_top_(left|right) (#8880)

pechersky committed 4 years ago

11e30477

feat(data/nat/totient): add nat.totient_prime_iff (#8833)

Ruben-VandeVelde committed 4 years ago

e2905697

feat(data/finset/pi_induction): induction on `Π i, finset (α i)` (#8794)

urkud committed 4 years ago

080362d0

feat(data/multiset/basic): add some lemmas (#8787)

Ruben-VandeVelde committed 4 years ago

83490fcd

feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field (#8762)

Vierkantor committed 4 years ago

d9f47130

chore(category/grothendieck): split definition to avoid timeout (#8871)

kim-em committed 4 years ago

5a2082d0

feat(analysis/normed_space/inner_product): multiplication by I is real-orthogonal (#8852)

hrmacbeth committed 4 years ago

9038709e

feat(ring_theory/ideal/local_ring): Isomorphisms are local (#8850)

justus-springer committed 4 years ago

5bd69fdf

feat(data/fin): reverse_induction (#8845)

ChrisHughes24 committed 4 years ago

5afdaea4

feat(data/list,multiset,finset): monotone_filter_(left|right) (#8842)

pechersky committed 4 years ago

678a2b5b

feat(tactic/lint/misc): Add syntactic tautology linter (#8821)

alexjbest committed 4 years ago

8e87f426

feat(data/fin): add_cases (#8876)

ChrisHughes24 committed 4 years ago

70e1f9a6

chore(archive/imo/README): whitespace breaks links (#8874)

kim-em committed 4 years ago

976e9306

chore(data/set): add a few lemmas and `@[simp]` attrs (#8873)

urkud committed 4 years ago

0d07d04e

feat(*): remove the `fintype` requirement from matrices. (#8810)

ericrbg committed 4 years ago

1f13610e

refactor(*): move code about `ulift`/`plift` (#8863)

urkud committed 4 years ago

0861cc75

refactor(order/filter/bases): allow `ι : Sort*` (#8856)

urkud committed 4 years ago

2a6fef39

Newer Older