leanprover-community/mathlib

Pull Requests Commits

chore(topology/algebra/ordered/*): Rename folder (#11988)

YaelDillies committed 4 years ago

1b5f8c28

chore(category_theory/monad/equiv_mon): Removing some slow uses of `obviously` (#11980)

stuart-presnell committed 4 years ago

7bebee66

chore(topology/algebra/module/multilinear): relax typeclass arguments (#11972)

eric-wieser committed 4 years ago

71e90063

refactor(measure_theory/group/basic): rename and split (#11952)

fpvandoorn committed 4 years ago

822244f7

feat(topology/instances/real): metric space structure on nat (#11963)

sgouezel committed 4 years ago

60d32337

more doc fixing

dupuisf committed 4 years ago

4cfc38a7

dupuisf committed 4 years ago

c1dafbdc

protected lemma

dupuisf committed 4 years ago

d5caeba8

dupuisf committed 4 years ago

124bc468

define normal elements of a star additive group

dupuisf committed 4 years ago

2bc2eaae

feat(tactic/lint): add unprintable tactic linter (#11725)

digama0 committed 4 years ago

dff8393c

feat(category_theory/category/Twop): The category of two-pointed types (#11844)

YaelDillies committed 4 years ago

227293b5

chore(order/cover): Rename `covers` to `covby` (#11984)

YaelDillies committed 4 years ago

788240cf

doc(data/finset/basic): correct some function names (#11983)

kmill committed 4 years ago

3fcb7380

refactor(data/nat/factorization): Use factorization instead of factors.count (#11384)

b-mehta committed 4 years ago

515ce797

feat(measure_theory/measure/haar_quotient): Pushforward of Haar measure is Haar (#11593)

AlexKontorovich committed 4 years ago

da76d218

feat(number_theory/number_field/basic) : the ring of integers of a number field is not a field (#11956)

mariainesdff committed 4 years ago

edefc116

feat(measure_theory/function/ae_eq_of_integral): remove a few unnecessary `@` (#11974)

RemyDegenne committed 4 years ago

1b78b4d1

fix(algebra/monoid_algebra/basic): remove an instance that forms a diamond (#11918)

eric-wieser committed 4 years ago

114752ca

feat(model_theory/direct_limit): Direct limits of first-order structures (#11789)

awainverse committed 4 years ago

492393b0

feat(data/pi): provide `pi.mul_single` (#11849)

nomeata committed 4 years ago

024aef0b

fix(ring_theory/algebraic): prove a diamond exists and remove the instances (#11935)

eric-wieser committed 4 years ago

8c60a927

chore(data/real/ennreal, topology/instances/ennreal): change name of the order isomorphism for `inv` (#11959)

j-loreaux committed 4 years ago

fbfdff7e

chore(algebra/star): generalize star_bit0, add star_inv_of (#11951)

eric-wieser committed 4 years ago

ae14f6ad

feat(topology/algebra/group): added (right/left)_coset_(open/closed) (#11876)

Sebastian-Monnet committed 4 years ago

0227820c

refactor(order/well_founded, set_theory/ordinal_arithmetic): Fix namespace in `self_le_of_strict_mono` (#11871)

vihdzp committed 4 years ago

73513580

chore(number_theory/cyclotomic/zeta): generalize to primitive roots (#11941)

ericrbg committed 4 years ago

4a5728fe

feat(algebra/big_operators): add prod_multiset_count_of_subset (#11919)

Ruben-VandeVelde committed 4 years ago

d487230d

feat(algebra/module/basic): turn implications into iffs (#11937)

fpvandoorn committed 4 years ago

fb41da97

feat(group_theory/group_action/defs): add ext attributes (#11936)

eric-wieser committed 4 years ago

09293874

Newer Older