leanprover-community/mathlib

Pull Requests Commits

chore(data/nat/cast): remove spurious imports

kim-em committed 3 years ago

d41e9916

feat(measure_theory/measure/measure_space): Add parallel set of lemmas about count (#17245)

kkytola committed 3 years ago

a0381d50

feat(representation_theory/fdRep): Schur's lemma (#13794)

kim-em committed 3 years ago

b9430470

feat(group_theory/index): add 3 lemmas (#17288)

urkud committed 3 years ago

2fc49d57

chore(algebra/order/group/basic): Improve lemma names (#16970)

YaelDillies committed 3 years ago

402f8982

feat(category_theory): nat_trans.equiv_of_comp_fully_faithful (#17304)

joelriou committed 3 years ago

51c07ea9

feat(category_theory/limits/shapes/*): More API around kernel pairs. (#17301)

erdOne committed 3 years ago

f6bab678

feat(representation_theory): fdRep k G is k-linear with finite dimensional hom spaces (#13789)

kim-em committed 3 years ago

ee89acdf

feat(category_theory/limits/shapes/types): Coproducts in `Type` (#17280)

erdOne committed 3 years ago

f020f410

feat(order/topology/filter): define topology on `filter X` (#17219)

urkud committed 3 years ago

78e50d8f

feat(finite_dimensional/subalgebra) : add subalgebra.is_simple_order_of_finrank (#17237)

xroblot committed 3 years ago

6d8e6ead

feat(linear_algebra/affine_space/basis): add `affine_basis.finite_dimensional` (#17246)

urkud committed 3 years ago

aae5e52b

feat(category_theory/triangulated): changing namespaces, introducing triangulated categories (#17284)

joelriou committed 3 years ago

19786714

feat(order/upper_lower): Upper sets correspond to monotone predicates (#17241)

YaelDillies committed 3 years ago

c64b2b4b

chore(data/nat/basic): reorder arguments to `nat.even_odd_rec` to make it work with `induction` (#17165)

eric-wieser committed 3 years ago

57035e18

chore(*): fix some to_additive orders (#17297)

alexjbest committed 3 years ago

b566cd5a

feat(analysis/normed/group/basic): closure of `{0}` in a seminormed group (#17287)

ADedecker committed 3 years ago

fdc3136d

feat(linear_algebra): lemmas and instances on cardinality of quotients (#17084)

Vierkantor committed 3 years ago

7e2084a7

feat(ring_theory/dedekind_domain): `gcd_monoid (ideal A)` in Dedekind domains (#17100)

Vierkantor committed 3 years ago

ee18af19

feat(group_theory/commutator): Define the set of commutators (#17276)

tb65536 committed 3 years ago

bdfa72be

feat(algebraic_geometry/prime_spectrum/basic): new lemmas + golf (#17289)

alreadydone committed 3 years ago

6fa3fc3e

feat(analysis/normed/group/pointwise): Multiplicativise (#17023)

YaelDillies committed 3 years ago

6cadbc0d

feat(algebra/order/field): Uniform bound in pi types (#16971)

YaelDillies committed 3 years ago

e1128562

feat(measure_theory/group/fundamental_domain): a large set contains 2 pts of the same orbit (#17293)

urkud committed 3 years ago

06eca3e1

feat(data/finite/card): Cardinality of union, image, and range (#17253)

tb65536 committed 3 years ago

a477dfd3

feat(group_theory/complement): The index of a complement of `H` equals the cardinality of `H` (#17250)

tb65536 committed 3 years ago

3256cf69

feat(data/real/cau_seq): Make power elementwise (#17124)

YaelDillies committed 3 years ago

3ede6d9e

chore(group_theory/semidirect_product): don't use private defs (#17290)

urkud committed 3 years ago

6ee5a076

feat(topology/subset_properties): upgrade `is_(pre)irreducible.closure` to iff (#17254)

alreadydone committed 3 years ago

226ea0fd

feat(measure_theory/measurable_space): add `measurable_of_countable` (#17266)

RemyDegenne committed 3 years ago

c5b46faa

Older