leanprover-community/mathlib

Pull Requests Commits

ADedecker committed 3 years ago

f1e01407

Go back to filters

ADedecker committed 3 years ago

389663c1

ADedecker committed 3 years ago

74a0159e

ADedecker committed 3 years ago

a07e00f0

ADedecker committed 3 years ago

c7e5d536

Merge branch 'bornology_order' into AD_uniform_convergence

ADedecker committed 3 years ago

a3a519a3

ADedecker committed 3 years ago

fd112611

Yael's suggestions

ADedecker committed 3 years ago

04fab1fc

feat(measure_theory/measure/measure_space): remove measurable_set assumption in ae_measurable.subtype_mk (#12978)

sgouezel committed 3 years ago

d620ad3c

chore(model_theory/*): Split up big model theory files (#12918)

awainverse committed 3 years ago

2c6df07f

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

leanprover-community-bot committed 3 years ago

57a5fd72

chore(data/set/intervals/ord_connected): Golf proof (#12923)

vihdzp committed 3 years ago

664247fc

refactor(topology/instances/ennreal): make `ennreal` an instance of `has_continuous_inv` (#12806)

j-loreaux committed 3 years ago

05ef6940

refactor(category_theory/abelian): deduplicate definitions of (co)image (#12902)

kim-em committed 3 years ago

caf6f192

feat(ring_theory/polynomial/eisenstein): add cyclotomic_prime_pow_comp_X_add_one_is_eisenstein_at (#12707)

riccardobrasca committed 3 years ago

f5a9d0a3

Module docstring

ADedecker committed 3 years ago

36139b0a

ADedecker committed 3 years ago

10ff0c3e

ADedecker committed 3 years ago

5291091e

refactor(data/list/basic): Remove many redundant hypotheses (#12950)

vihdzp committed 3 years ago

7b938899

feat(algebra/ring/basic): all non-zero elements in a non-trivial ring with no non-zero zero divisors are regular (#12947)

adomani committed 3 years ago

e63e3322

fix(data/set/prod): fix the way `×ˢ` associates (#12943)

fpvandoorn committed 3 years ago

b30f25ce

chore(data/equiv): split and move to `logic/equiv` (#12929)

Vierkantor committed 3 years ago

cc8c90d4

feat(analysis/convex/strict_convex_space): Strictly convex spaces (#11794)

YaelDillies committed 3 years ago

434a938b

chore(order/filter/basic): rename using the zero subscript convention for groups with zero (#12952)

sgouezel committed 3 years ago

1f11f3f3

chore(measure_theory/integral/lebesgue): extend to ae_measurable (#12953)

sgouezel committed 3 years ago

a491055c

feat(measure_theory/constructions/borel_space): drop a countability assumption (#12954)

sgouezel committed 3 years ago

cb2797ee

chore(measure_theory/measure/lebesgue): delete leftovers (#12951)

sgouezel committed 3 years ago

b7d9166a

feat(topology/bases): separable subsets of topological spaces (#12936)

sgouezel committed 3 years ago

11114823

feat(topology/constructions): continuity of uncurried functions when the first factor is discrete (#12935)

sgouezel committed 3 years ago

f68536e0

feat(algebra/is_prime_pow): add `is_prime_pow_iff_factorization_single` (#12167)

stuart-presnell committed 3 years ago

5e449c20

Older