leanprover-community/mathlib

Pull Requests Commits

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)

github-actions[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

chore(algebra/big_operators/part_enat): drop file (#17934)

urkud committed 3 years ago

a2efed67

feat(data/prod/basic): `prod.lex` is trichotomous (#17931)

YaelDillies committed 3 years ago

198161d8

feat(data/fin/basic): lemmas commuting `cast_add` and `nat_add` (#17917)

eric-wieser committed 3 years ago

d97d4fac

refactor(data/set/intervals): Generalize `set.interval` to lattices (#17776)

YaelDillies committed 3 years ago

b8858394

Revert "feat(ring_theory/power_series): `X s` commutes with any power series"

urkud committed 3 years ago

27982536

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

urkud committed 3 years ago

f1adf6ad

chore(group_theory/group_action/prod): Fix typo in `to_additive` attribute. (#17930)

adamtopaz committed 3 years ago

46ae64dc

feat(data/set/n_ary): Distributivity of `∩` (#17924)

YaelDillies committed 3 years ago

4a1bf948

Newer Older