leanprover-community/mathlib

Pull Requests Commits

feat(linear_algebra): linear_equiv_matrix lemmas (#3898)

PatrickMassot committed 5 years ago

aca785a7

feat(category_theory/opposites): isomorphism of opposite functor (#3901)

b-mehta committed 5 years ago

e9d10674

feat(set_theory/game): impartial games and the Sprague-Grundy theorem (#3855)

foxthomson committed 5 years ago

011a2622

fix(data/equiv/transfer_instance): remove stray #lint (#3908)

bryangingechen committed 5 years ago

e546e946

feat(tactic/dec_trivial): make dec_trivial easier to use (#3875)

jcommelin committed 5 years ago

13881d7a

feat(algebra/group/with_one): make with_one and with_zero irreducible. (#3883)

kbuzzard committed 5 years ago

83db96b2

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

leanprover-community-bot committed 5 years ago

4b241664

feat(data/real): define the golden ratio and its conjugate, prove irrationality of both and Binet's formula (#3885)

ADedecker committed 5 years ago

278f5120

chore(measure_theory/*): remove some `measurable f` arguments (#3902)

urkud committed 5 years ago

9998bee7

feat(topology/algebra/ordered): sum of functions with limits at_top and cst (#3833)

hrmacbeth committed 5 years ago

4c04f0bb

feat(set/basic): some results about `set.pi` (#3894)

fpvandoorn committed 5 years ago

1db32c59

feat(measure_theory/bochner_integration): add `integral_smul_measure` (#3900)

urkud committed 5 years ago

0c7ac835

feat(order/rel_iso): a new definition of order_iso, using preorder instances (#3838)

awainverse committed 5 years ago

ac567902

feat(data/zmod/basic): morphisms to zmod are surjective (deps: #3888) (#3889)

jcommelin committed 5 years ago

e3409c6c

feat(analysis/special_functions/arsinh): inverse hyperbolic sine function (#3801)

JamesAMaths committed 5 years ago

4921be9d

feat(logic/function): left/right inverse iff (#3897)

PatrickMassot committed 5 years ago

7a48761e

feat(group_theory/subroup,ring_theory/ideal/operations): lift_of_surjective (#3888)

jcommelin committed 5 years ago

de20a394

chore(topology/basic): use dot notation (#3861)

urkud committed 5 years ago

045b6c7f

feat(measure_theory/interval_integral): more versions of FTC-1 (#3709)

urkud committed 5 years ago

d8cde2aa

feat(tactic/rcases): clear pattern `-` in rcases (#3868)

digama0 committed 5 years ago

bc3e8356

feat(determinant): towards multilinearity (#3887)

PatrickMassot committed 5 years ago

da6cd551

chore(measure_theory/*): use `_measure` instead of `_meas` (#3892)

urkud committed 5 years ago

23749aa0

chore(order/bounded_lattice): use `⦃⦄` in `disjoint.symm` (#3893)

urkud committed 5 years ago

31cd6dd2

feat(category_theory/monad/*): Add category of bundled (co)monads; prove equivalence of monads with monoid objects (#3762)

adamtopaz committed 5 years ago

17190352

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

leanprover-community-bot committed 5 years ago

7271f74f

feat(system/random): a monad for (pseudo-)randomized computations (#3742)

cipher1024 committed 5 years ago

0a48f0a2

feat(linear_algebra): some easy linear map/equiv lemmas (#3890)

PatrickMassot committed 5 years ago

36386fc7

chore(data/matrix, linear_algebra): generalize universe parameters (#3879)

Vierkantor committed 5 years ago

c9704ff5

feat(ring_theory/separable): a separable polynomial splits into a product of unique `X - C a` (#3877)

Vierkantor committed 5 years ago

901c5bca

chore(category_theory/limits/types): cleanup (#3871)

kim-em committed 5 years ago

9f525c74

Newer Older