leanprover-community/mathlib

Pull Requests Commits

chore(*): remove extra parentheses in universe annotations (#14595)

vihdzp committed 3 years ago

201a3f4a

feat(algebra/algebra/basic): add instances `char_zero.no_zero_smul_divisors_int`, `char_zero.no_zero_smul_divisors_nat` (#14395)

ocfnash committed 3 years ago

3e4d6aa3

feat(logic/basic): add lemma `pi_congr` (#14616)

adomani committed 3 years ago

bfb8ec83

refactor(algebra/is_prime_pow): move lemmas using `factorization` to new file (#14598)

stuart-presnell committed 3 years ago

700181a3

doc(data/qpf/multivariate/constructions/cofix): fix doc typos (#14609)

vihdzp committed 3 years ago

db4531fa

chore(set_theory/cardinal/basic): remove unused universe + fix spacing (#14606)

vihdzp committed 3 years ago

0add8768

feat(algebra/lie/centralizer): define the centralizer of a Lie submodule and the upper central series (#14173)

ocfnash committed 3 years ago

65fba4cb

golf(*): `λ _, default` → `default` (#14608)

vihdzp committed 3 years ago

ffad43d2

feat(algebra/order/monoid): `zero_le_one'` lemma with explicit type argument (#14594)

vihdzp committed 3 years ago

60454dd3

feat(topology/algebra/order/basic): in a second-countable linear order, only countably many points are isolated to the right (#14564)

sgouezel committed 3 years ago

f40cd3cf

feat(group_theory/sylow): The index of a sylow subgroup is indivisible by the prime (#14518)

tb65536 committed 3 years ago

a20032ac

feat(topology/continuous_function/compact): `cstar_ring` instance on `C(α, β)` when `α` is compact (#14437)

dupuisf committed 3 years ago

54236f5a

chore(data/finset): remove duplicated lemma (#14607)

b-mehta committed 3 years ago

e39af181

feat(data/int/basic): Sum of units casework lemma (#14557)

tb65536 committed 3 years ago

9d048443

chore(ring_theory/dedekind_domain/ideal): speed up a proof (#14590)

alreadydone committed 3 years ago

759516c7

feat(special_functions/gamma): better convergence bounds (#14496)

khwilson committed 3 years ago

905374c4

chore(logic/hydra): tweak docs + minor golf (#14579)

vihdzp committed 3 years ago

cfa447ec

refactor(topology/continuous_function/basic): rename `map_specialization` (#14565)

urkud committed 3 years ago

43f1af99

chore(ring_theory/integral_closure): fix dot notation (#14589)

ericrbg committed 3 years ago

544fdc0d

refactor(algebra/squarefree): split out `nat` part to new file `data/nat/squarefree` (#14577)

stuart-presnell committed 3 years ago

69066273

feat(topology/metric_space/metrizable): assume `regular_space` (#14586)

urkud committed 3 years ago

4a4cd6d6

chore(set_theory/game/basic): spacing tweaks + fix docstring typo (#14580)

vihdzp committed 3 years ago

de648fd5

feat(set_theory/game/pgame): induction on left/right moves of add/mul (#14345)

vihdzp committed 3 years ago

6ad1a55f

feat(measure_theory/measure/measure_space): add `interval_oc_ae_eq_interval` (#14566)

urkud committed 3 years ago

c7a1319b

chore(geometry/manifold/charted_space): make `M` an explicit argument (#14562)

urkud committed 3 years ago

2c893060

refactor(analysis/asymptotics): rename `is_O.join` to `is_O.sup` (#14558)

urkud committed 3 years ago

d0b7ecc9

feat(order/liminf_limsup): add a few lemmas (#14554)

urkud committed 3 years ago

2b7e72b0

refactor(../metric_space/baire): add baire_space class and instances (#14547)

D-Thomine committed 3 years ago

029a9551

feat(analysis/normed_space/banach): closed graph theorem (#14265)

ADedecker committed 3 years ago

d28aa2c9

feat(algebra/order/*): typeclass for `0 ≤ 1` (#14510)

vihdzp committed 3 years ago

7b7da893

Newer Older