leanprover-community/mathlib3

Pull Requests Commits

generalize to pseudo_metric_space

fpvandoorn committed 3 years ago

893823aa

feat(measure_theory/group/*): various lemmas about invariant measures (#13539)

fpvandoorn committed 3 years ago

95413e23

feat(analysis/special_functions/trigonometric): add a lemma (#13975)

urkud committed 3 years ago

ebac9f03

feat(model_theory/*): Any theory with infinite models has arbitrarily large models (#13980)

awainverse committed 3 years ago

faf16900

chore(algebra/ring/idempotents): golf iff_eq_zero_or_one (#13977)

Ruben-VandeVelde committed 3 years ago

f0eded9a

feat(algebra/group/defs): Division monoids (#13860)

YaelDillies committed 3 years ago

151933d1

feat(model_theory/skolem): Downward Löwenheim–Skolem (#13723)

awainverse committed 3 years ago

c62dfe61

feat(linear_algebra/basic): ker of a linear map equals ker of the corresponding group hom (#13858)

ADedecker committed 3 years ago

91cc3f06

fix(gitpod): correct command name (#13976)

eric-wieser committed 3 years ago

c12536a7

feat(analysis/special_functions/exp): add limits of `exp z` as `re z → ±∞` (#13974)

urkud committed 3 years ago

73e5dadd

fix(topology/algebra/infinite_sum): `tsum_neg` doesn't need `summable` (#13950)

kbuzzard committed 3 years ago

54af9e9b

feat(data/matrix/basic): even more lemmas about `conj_transpose` and `smul` (#13970)

eric-wieser committed 3 years ago

ec44f459

chore(analysis/normed_space/exponential): replace `1/x` with `x⁻¹` (#13971)

eric-wieser committed 3 years ago

420fabf7

feat(category_theory/simple): simple_iff_subobject_is_simple_order (#13969)

kim-em committed 3 years ago

03f5ac93

refactor(ring_theory/*): Remove unnecessary commutativity assumptions (#13966)

haruhisa-enomoto committed 3 years ago

929c9018

feat(polynomial/cyclotomic/basic): ɸ_pⁱ irreducible → ɸ_pʲ irreducible for j ≤ i (#13952)

ericrbg committed 3 years ago

8e0ab168

feat(linear_algebra/finite_dimensional): surjective_of_nonzero_of_finrank_eq_one (#13961)

kim-em committed 3 years ago

057e0283

feat(linear_algebra): A-linear maps between finite dimensional vector spaces over k are finite dimensional (#13934)

kim-em committed 3 years ago

da06587c

feat({data/{finset,set},order/filter}/pointwise): More basic API (#13899)

YaelDillies committed 3 years ago

4dfbcac3

ci(gitpod): do not rerun get-cache if a workspace is reloaded (#13949)

eric-wieser committed 3 years ago

f8206717

chore(algebra/group/units): add a lemma about is_unit on a coerced unit (#13947)

eric-wieser committed 3 years ago

69701295

chore(linear_algebra/free_module): fix name in doc (#13942)

alexjbest committed 3 years ago

bd944fe1

chore(data/matrix/basic): add more lemmas about `conj_transpose` and `smul` (#13938)

eric-wieser committed 3 years ago

4f7603c7

feat(analysis/normed/normed_field): limit of `∥a * x∥` as `∥x∥ → ∞` (#13819)

urkud committed 3 years ago

7eacca31

Update CODE_OF_CONDUCT.md (#13965)

madvorak committed 3 years ago

03fbe7de

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

leanprover-community-bot committed 3 years ago

63875eae

feat(tactic/alias): fix alias docstrings for implications from iffs (#13944)

alexjbest committed 3 years ago

116435d6

feat(representation_theory): Action V G is rigid whenever V is (#13738)

kim-em committed 3 years ago

524793de

feat(data/sum/basic): Shortcuts for the ternary sum of types (#13678)

YaelDillies committed 3 years ago

b1da074a

feat(algebra/group/{pi, opposite}): add missing pi and opposite defs for `mul_hom` (#13956)

j-loreaux committed 3 years ago

0c9b7263

Older