leanprover-community/mathlib

Pull Requests Commits

Split `infinite_of_mem_nhds` to extract a useful lemma (#17971)

ADedecker committed 3 years ago

dcf22508

feat(ring_theory/ideal/local_ring): add lemmas about local_ring.residue_field.map (#17969)

mkaratarakis committed 3 years ago

758a6a4e

chore(number_theory/divisors): golf (#17954)

urkud committed 3 years ago

c2337ec8

feat(combinatorics/quiver/*): More edge reversal constructions (#17665)

bottine committed 3 years ago

706d88f2

feat(measure_theory/integral/layercake): Add versions of layercake formula with strict inequality. (#17920)

kkytola committed 3 years ago

11bb0c91

feat(measure_theory/measure/measure_space): A `measurable_equiv` is `quasi_measure_preserving` (#17774)

YaelDillies committed 3 years ago

2c5df64a

feat(dynamics/ergodic/ergodic): expand ergodic map API for finite measures (#17864)

ocfnash committed 3 years ago

809e920e

refactor(measure_theory/group/fundamental_domain): Use `pairwise` (#17928)

YaelDillies committed 3 years ago

d5ca915d

chore(order/monovary): Move (#17946)

YaelDillies committed 3 years ago

b3f25363

feat(measure_theory/covering) weaken sigma_compact_space to second_countable_topology (#17960)

sgouezel committed 3 years ago

d012cd09

chore(data/finset/lattice): Protect ambiguous lemmas (#17938)

YaelDillies committed 3 years ago

302eab4f

feat(combinatorics/simple_graph/*): some more `from_edge_set` and `edge_set` lemmas (#17723)

bottine committed 3 years ago

e3a8dff0

fix(algebra/opposites): fix types in unop_div (#17955)

kbuzzard committed 3 years ago

ac3910d7

chore(data/set/image): Turn lemma around (#17945)

YaelDillies committed 3 years ago

616e053d

chore(number_theory/arithmetic_function): golf (#17953)

urkud committed 3 years ago

49420fb1

feat(data/finset/basic): `finset α` is well-founded (#17950)

YaelDillies committed 3 years ago

33daf353

feat(order/basic): Checking associativity in partial order (#17942)

YaelDillies committed 3 years ago

633c32ea

feat(logic/lemmas): `(∀ p, f p) ↔ f true ∧ f false` (#17944)

YaelDillies committed 3 years ago

4237da0f

chore(*): add mathlib4 synchronization comments (#17943)

leanprover-community-bot committed 3 years ago

a59dad53

fix(geometry/euclidean/angle/unoriented/right_angle): fix lemma naming (#17941)

jsm28 committed 3 years ago

0efabe73

fix(ci/add_ported_warnings): use a version of the action that does not error (#17936)

eric-wieser committed 3 years ago

2f7913bd

feat(algebra/star/basic): add ring_hom.has_involutive_star (#17904)

xroblot committed 3 years ago

daf8adf1

feat(combinatorics/double_counting): Special cases (#17647)

YaelDillies committed 3 years ago

aba57d4d

feat(order/succ_pred/basic): `a ⩿ b → b ≤ succ a` (#17940)

YaelDillies committed 3 years ago

f2c46488

feat(ring_theory/power_series): `X s` commutes with any power series (#17935)

urkud committed 3 years ago

7d6cd041

feat(dynamics/ergodic/add_circle): generalise `add_circle.ae_empty_or_univ_of_forall_vadd_eq_self` slightly (#17907)

ocfnash committed 3 years ago

ae3588fa

feat(measure_theory/covering/liminf_limsup): add lemma `blimsup_cthickening_mul_ae_eq` (#17803)

ocfnash committed 3 years ago

1897d7de

fix(tactic/assert_exists): use more unique names (#17916)

eric-wieser committed 3 years ago

90367774

feat(ring_theory/dedekind_domain/factorization): add factorization lemmas (#17915)

mariainesdff committed 3 years ago

ae0d10f6

feat(data/set/pointwise/smul): `a • (s \ t) = a • s \ a • t` (#17927)

YaelDillies committed 3 years ago

ae193735

Newer Older