leanprover-community/mathlib

Pull Requests Commits

jjaassoonn committed 3 years ago

76a1b696

Update imo1979_q1.lean

MantasBaksys committed 4 years ago

52b5cbf4

Merge branch 'master' into imo1979q1

MantasBaksys committed 4 years ago

36748541

chore(topology,measure_theory): generalize a few instances (#9967)

urkud committed 4 years ago

415da222

feat(archive/imo): IMO 2021 Q1 (#8432)

MantasBaksys committed 4 years ago

0cfae438

feat(ring_theory/adjoin_root): golf and generalize the algebra structure on `adjoin_root` (#10019)

eric-wieser committed 4 years ago

99a2d5bf

feat(data/finset/interval): Bounded intervals in locally finite orders are finite (#9960)

YaelDillies committed 4 years ago

18dce134

feat(list): add some lemmas (#9873)

EPronovost committed 4 years ago

17339204

feat(data/set/function): restrict `dite/ite/piecewise/extend` (#10017)

urkud committed 4 years ago

e927aa4e

chore(*): a few lemmas about `range_splitting (#10016)

urkud committed 4 years ago

0d6548fc

chore(measure_theory/measure/measure_space): reorder, golf (#10015)

urkud committed 4 years ago

b9ff26b5

feat(order/bounded_lattice): add `is_compl.le_sup_right_iff_inf_left_le` (#10014)

urkud committed 4 years ago

fd6f6816

fix(field_theory/intermediate_field): use a better `algebra.smul` definition, and generalize (#10012)

eric-wieser committed 4 years ago

22d32dcd

feat(group_theory/subgroup/basic): `mul_mem_sup` (#10007)

tb65536 committed 4 years ago

fe76b5c0

move(data/set/pairwise): Move `set.pairwise_on` (#9986)

YaelDillies committed 4 years ago

c495ed61

feat(computability/tm_to_partrec): prove finiteness (#6955)

digama0 committed 4 years ago

628f418d

feat(data/{finset,multiset}/locally_finite): Simple interval lemmas (#9877)

YaelDillies committed 4 years ago

c8d14294

feat(analysis/normed_space/pi_Lp): use typeclass inference for `1 ≤ p` (#9922)

hrmacbeth committed 4 years ago

acbb2a53

chore(measure_theory): a `continuous_map` is measurable (#9998)

urkud committed 4 years ago

b0349aa9

feat(measure/measurable_space): add `measurable_equiv.of_unique_of_unique` (#9968)

urkud committed 4 years ago

73423cf9

feat(analysis/inner_product_space/dual): complex Riesz representation theorem (#9924)

hrmacbeth committed 4 years ago

7f2b8064

feat(category_theory/arrow): is_iso, mono, epi instances for maps between arrows (#9976)

jcommelin committed 4 years ago

f78b7398

feat(measure_theory/construction/borel_space): two measures are equal if they agree on closed-open intervals (#9396)

kex-y committed 4 years ago

8159af67

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

leanprover-community-bot committed 4 years ago

468a9d56

fix(data/equiv/encodable): turn `unique.encodable` into a `def` (#10006)

urkud committed 4 years ago

bcaeb57a

chore(*): rename gsmul to zsmul and gmultiples to zmultiples (#10010)

sgouezel committed 4 years ago

9db72700

feat(linear_algebra/free_module/finite/rank): add linear_algebra/free_module/finite/rank (#9832)

riccardobrasca committed 4 years ago

d360f3cb

feat(algebra/order/archimedean): a few more lemmas (#9997)

urkud committed 4 years ago

8ce5da4b

chore(algebra/order/floor): prove `subsingleton`s (#9996)

urkud committed 4 years ago

ec51fb79

feat(group_theory/group_action/conj_act): A characteristic subgroup of a normal subgroup is normal (#9992)

tb65536 committed 4 years ago

eaec1dae

Older