Commits leanprover-community/mathlib

refactor(data/finset/nat_antidiagonal): state lemmas with cons instead of insert (#14533)

eric-wieser committed 3 years ago

4fc35392

chore(data/set/basic): minor style fixes (#14628)

vihdzp committed 3 years ago

0c08bd43

feat(linear_algebra/affine_space/affine_subspace/pointwise): Translations are an action on affine subspaces (#14230)

winston-h-zhang committed 3 years ago

c1faa2ee

refactor(topology/metric_space/basic): add `pseudo_metric_space.to_bornology'` (#13927)

urkud committed 3 years ago

84a1bd6a

feat(set_theory/ordinal/basic): tweak `type_def` + golf `type_lt` (#14611)

vihdzp committed 3 years ago

61df9c66

feat(ring_theory/valuation/valuation_subring): define unit group of valuation subring and provide basic API (#14540)

mckoen committed 3 years ago

9c4a3d1b

feat(model_theory/substructures): tweak universes for `lift_card_closure_le` (#14597)

vihdzp committed 3 years ago

d3156667

feat(set_theory/ordinal/basic): `rel_iso.ordinal_type_eq` (#14602)

vihdzp committed 3 years ago

89348848

feat(order/rel_classes): any relation on an empty type is a well-order (#14600)

vihdzp committed 3 years ago

09df85f6

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