leanprover-community/mathlib

Pull Requests Commits

urkud committed 4 years ago

14f1dd7b

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

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

RemyDegenne committed 4 years ago

70ed9dce

feat(algebra/big_operators/order): add unbundled is_absolute_value.sum_le and map_prod (#10104)

alexjbest committed 4 years ago

d43daf01

feat(data/bool): bnot_iff_not (#10095)

TwoFX committed 4 years ago

3accc5ed

feat(logic/relation): add equivalence.comap (#10103)

eric-wieser committed 4 years ago

00064bd6

chore(measure_theory/probability_mass_function): avoid non-terminal simp in coe_le_one (#10112)

Ruben-VandeVelde committed 4 years ago

2d8be73e

Older