leanprover-community/mathlib3

Pull Requests Commits

feat(data/nat/choose/basic): add some inequalities showing that choose is monotonic in the first argument (#10102)

alexjbest committed 4 years ago

211bdff0

feat(data/list): standardize list prefixes and suffixes (#10052)

EPronovost committed 4 years ago

1f0d878c

feat(topology/homotopy/basic): add `homotopic` for `continuous_map`s. (#9865)

shingtaklam1324 committed 4 years ago

4c0b6ada

chore(data/equiv/mul_add): DRY (#10150)

urkud committed 4 years ago

d219e6bb

chore(ring_theory/finiteness): make `finite_presentation.{quotient,mv_polynomial}` protected (#10091)

eric-wieser committed 4 years ago

76ba1b64

feat(algebra/group_power/order): Sign of an odd/even power without linearity (#10122)

YaelDillies committed 4 years ago

8658f40c

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

leanprover-community-bot committed 4 years ago

4770a6a7

refactor(analysis/calculus/mean_value): Remove useless hypotheses (#10129)

YaelDillies committed 4 years ago

0fac0807

refactor(algebra/direct_sum): rework internally-graded objects (#10127)

eric-wieser committed 4 years ago

fed57b54

feat(group_theory/sylow): Sylow subgroups are isomorphic (#10059)

tb65536 committed 4 years ago

6433c1c6

refactor(group_theory/complement): Introduce abbreviation for subgroups (#10009)

tb65536 committed 4 years ago

5541b256

chore(order/lattice): add `exists_lt_of_sup/inf` (#10133)

urkud committed 4 years ago

3a0b0d1d

chore(analysis/special_functions/trigonometric/inverse): move results about derivatives to a new file (#10110)

RemyDegenne committed 4 years ago

8f7ffec9

chore(logic/relation): rename to permit dot notation (#10105)

eric-wieser committed 4 years ago

00a1022f

feat(measure_theory/constructions/borel_space): decomposing the measure of a set into slices (#10096)

sgouezel committed 4 years ago

6993e6f8

feat(topology): properties about intervals and paths (#9914)

fpvandoorn committed 4 years ago

b51f18f7

feat(measure_theory/function/ae_measurable_order): an ae measurability criterion for ennreal-valued functions (#10072)

sgouezel committed 4 years ago

8d52be4a

feat(analysis/seminorm): define the Minkowski functional (#9097)

YaelDillies committed 4 years ago

4f033b7d

doc(linear_algebra): fix wrong docstring (#10139)

PatrickMassot committed 4 years ago

95cdebac

feat(ring_theory/trace): remove a useless assumption (#10138)

riccardobrasca committed 4 years ago

2b87435a

chore(*): replace `exact calc` by `calc` (#10137)

jcommelin committed 4 years ago

93cec259

fix(scripts/lint-style.py): typo in error reporting (#10135)

jcommelin committed 4 years ago

eaf2a16b

feat(data/zmod/basic): add nat_coe_eq_nat_coe_iff' (#10128)

alexjbest committed 4 years ago

1e7f3ca6

chore(topology/continuous_function/bounded): add `comp_continuous` (#10134)

urkud committed 4 years ago

e5c66a09

chore(order/conditionally_complete_lattice): drop an unneeded `nonempty` assumption (#10132)

urkud committed 4 years ago

e5acda42

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

leanprover-community-bot committed 4 years ago

5f2e5270

feat(linear_algebra/determinant): basis.det_ne_zero (#10126)

jsm28 committed 4 years ago

123db5e8

chore(algebra/order/floor): add a few trivial lemmas (#10120)

urkud committed 4 years ago

86ed02f9

doc(topology): three module docstrings (#10107)

PatrickMassot committed 4 years ago

1dec85c5

doc(topology/open_subgroup): add module docstring (#10111)

PatrickMassot committed 4 years ago

d49636ec

Newer Older