leanprover-community/mathlib

Pull Requests Commits

astrainfinita committed 3 years ago

23ebadfb

Merge remote-tracking branch 'origin/FR_zero_lt_changes' into FR_zero_lt_changes_fail

astrainfinita committed 3 years ago

cf42bb58

fix `apply_instance` failure (hack?)

astrainfinita committed 3 years ago

ab1ef27a

astrainfinita committed 3 years ago

1e2fb18b

fix measure_theory\integral\set_to_l1

astrainfinita committed 3 years ago

6cbbb12a

feat(algebra/parity): Primes are not square (#16430)

YaelDillies committed 3 years ago

5e78882f

refactor(analysis/normed_space/spectrum): generalize Gelfand-Mazur away from `normed_division_ring` (#16448)

j-loreaux committed 3 years ago

ba6b1422

feat(probability/stopping): generalize `mem_ℒp_stopped_value` (#16369)

RemyDegenne committed 3 years ago

7fd4a0bf

fix `number_theory/class_number/finite`

astrainfinita committed 3 years ago

a19a5f5f

fix analysis/special_functions/bernstein

astrainfinita committed 3 years ago

fe34c106

use `ₚ` instead of `₀`

astrainfinita committed 3 years ago

e684fcdd

feat(counterexamples/sorgenfrey_line): new file (#14820)

urkud committed 3 years ago

f7d03fec

remove `zero_lt` in other file

astrainfinita committed 3 years ago

78e3224e

astrainfinita committed 3 years ago

a1a1eaab

feat(linear_algebra/linear_pmap): add_action and mul_action (#16068)

mcdoll committed 3 years ago

48e3d6a4

use `₀` to avoid conflicts and replace lemmas in `algebra.order.ring`

astrainfinita committed 3 years ago

2227ccc5

deal with namespaces

astrainfinita committed 3 years ago

b24c6f4c

remove useless lemmas

astrainfinita committed 3 years ago

37b8007d

make it consistent again...

astrainfinita committed 3 years ago

8e1befee

astrainfinita committed 3 years ago

293aefed

#16097, style only

astrainfinita committed 3 years ago

99d90ae6

astrainfinita committed 3 years ago

45c70aff

astrainfinita committed 3 years ago

4dd3cd43

name issues after #16189

astrainfinita committed 3 years ago

ae4d390d

feat(algebra/order/monoid_lemma_zero_lt): change tracking

astrainfinita committed 3 years ago

09a68447

feat(topology/algebra/module/weak_dual): `weak_space` is functorial (#16441)

ADedecker committed 3 years ago

22a9066d

feat(analysis/inner_product_space/basic): completion of an `inner_product_space` is an `inner_product_space` (#16407)

ADedecker committed 3 years ago

c3d2b3b8

feat(analysis/{normed/group}/seminorm): Hom classes for seminorms (#16227)

YaelDillies committed 3 years ago

3a0b839b

feat(analysis/normed/group/basic): add `norm_multiset_sum_le` (#16419)

astrainfinita committed 3 years ago

75cc1ae9

feat(order/upper_lower): `Iic` is not bounded below (#16425)

YaelDillies committed 3 years ago

ba346d8b

Older