leanprover-community/mathlib3

Pull Requests Commits

chore(analysis/normed_space/bounded_linear_maps): squeeze simps (#17368)

mcdoll committed 3 years ago

a9a490da

chore(linear_algebra/basic): squeeze non-terminal simps (#17367)

mcdoll committed 3 years ago

4bb16a67

chore(data/finsupp/basic): golf a lemma (#17366)

eric-wieser committed 3 years ago

654bbd9c

chore(linear_algebra/basic): add `linear_equiv.conj_apply_apply` (#17364)

eric-wieser committed 3 years ago

fbaa3ad0

chore(data/finsupp): move and rename `finsupp.single_apply_left` (#17357)

Vierkantor committed 3 years ago

34fb08a7

split(algebra/order/nonneg): Separate `ring` and `field` instances (#17348)

YaelDillies committed 3 years ago

43e01caf

feat(data/set/basic): add `set.subsingleton_range` (#17248)

urkud committed 3 years ago

d7da6980

refactor(data/set/pairwise): use `{{..}}` arguments (#17230)

urkud committed 3 years ago

00d450eb

feat(data/real/enat_ennreal): define coercion from `enat` to `ennreal` (#17207)

urkud committed 3 years ago

c48d7bfe

refactor(data/fun_like,logic/equiv): generalize instances (#17205)

urkud committed 3 years ago

1b9de287

feat(data/fintype/basic): a type is infinite if it admits an injective map to a proper subset (#17204)

urkud committed 3 years ago

614849cd

doc(citation.md): Add a citation.md file (#17202)

BoltonBailey committed 3 years ago

e8ecfea7

feat(category_theory/localization): localization of the opposite category (#17199)

joelriou committed 3 years ago

8efef279

refactor(algebra/free): review API, redefine `free_semigroup` (#17144)

urkud committed 3 years ago

c64b9224

feat(linear_algebra): membership of a submodule given a basis of the submodule (#17083)

Vierkantor committed 3 years ago

635bc8db

feat(order/order_iso_nat): value is accessible iff it's not contained in an infinite decreasing sequence (#15927)

vihdzp committed 3 years ago

fe664106

feat(set_theory/game/basic): generalize equivalences to relabellings (#15252)

vihdzp committed 3 years ago

4b788397

chore(data/nat/order): move some results about range succ (#17365)

Ruben-VandeVelde committed 3 years ago

228404df

chore(algebra/order/field): split out file about powers (#17352)

kim-em committed 3 years ago

f8f8be9a

chore(data/int/basic): split file (#17342)

kim-em committed 3 years ago

11613e28

chore(measure_theory/measure/finite_measure_weak_convergence): Split one file to three. (#17332)

kkytola committed 3 years ago

96e43cce

refactor(algebra/group_power/lemmas): assume `n ≠ 0` instead of `0 < n` (#17323)

urkud committed 3 years ago

03fda911

feat(geometry/manifold/*): "composition" of `charted_space` and `has_groupoid` instances (#17305)

hrmacbeth committed 3 years ago

688effb8

doc(analysis/locally_convex/with_seminorms): fix hyperlink and add first countable (#17303)

mcdoll committed 3 years ago

e4515446

doc(data/set/basic): add pointer to iff versions (#17300)

kmill committed 3 years ago

58b7f910

chore(data/list/count): use + 1 instead of nat.succ (#17161)

urkud committed 3 years ago

8b889832

feat(category_theory/groupoid/*): `is_thin` and `is_totally_disconnected` (#17122)

bottine committed 3 years ago

f187f107

feat(algebra/gcd_monoid/div): add finset.int.gcd_is_unit_of_div_gcd and similar results (#16838)

riccardobrasca committed 3 years ago

bf3b618e

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology (#16053)

ADedecker committed 3 years ago

b916d59f

feat(data/finset/basic): add lemmas about filter and (co)disjoint (#17296)

eric-wieser committed 3 years ago

7951ed37

Newer Older