leanprover-community/mathlib

Pull Requests Commits

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

chore(combinatorics/choose/bounds): move to nat namespace (#10106)

eric-wieser committed 4 years ago

6df3143a

style(testing/slim_check): fix line length (#10114)

PatrickMassot committed 4 years ago

0dcb1849

feat(measure_theory/decomposition/lebesgue): more on Radon-Nikodym derivatives (#10070)

sgouezel committed 4 years ago

796a051a

feat(data/mv_polynomial/basic): lemmas about map (#10092)

eric-wieser committed 4 years ago

da6706d0

refactor(order/bounded_lattice): generalize le on with_{top,bot} (#10085)

pechersky committed 4 years ago

80dc445d

refactor(algebra/algebra): remove subalgebra.under (#10081)

eric-wieser committed 4 years ago

658a3d77

feat(topology/algebra/ordered/liminf_limsup): convergence of a sequence which does not oscillate infinitely (#10073)

sgouezel committed 4 years ago

541df8a0

chore(analysis/normed/group): add `cauchy_seq_finset_of_norm_bounded_eventually` (#10060)

urkud committed 4 years ago

880182d6

feat(measure_theory/probability_mass_function): Define uniform pmf on an inhabited fintype (#9920)

dtumad committed 4 years ago

fc12ca8d

chore(ring_theory/adjoin/fg): generalize ring to semiring in a few places (#10089)

eric-wieser committed 4 years ago

f6894c47

chore(coinductive_predicates): remove private and use of import_private (#10084)

kim-em committed 4 years ago

26bdcac0

feat(analysis/calculus/mean_value): Strict convexity from derivatives (#10034)

YaelDillies committed 4 years ago

18528404

chore(data/list/defs): remove unneeded open (#10100)

kim-em committed 4 years ago

6d2af9a1

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

leanprover-community-bot committed 4 years ago

d926ac73

Newer Older