Commits leanprover-community/mathlib3

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

feat(order/extension/well): Extend a well-founded order (#17054)

YaelDillies committed 3 years ago

65ee8572

feat(data/real/ennreal): Positivity extension for `ennreal.of_real` (#16955)

YaelDillies committed 3 years ago

1ab3ae03

feat(probability/borel_cantelli): the second Borel-Cantelli lemma (#16882)

kex-y committed 3 years ago

1e7dab97

refactor(data/fintype/basic): simplify the defeq of `sum.fintype` (#17236)

eric-wieser committed 3 years ago

e2b33abb

chore(combinatorics/quiver/path): reduce imports (#17216)

kim-em committed 3 years ago

88bad67d

doc(ring_theory/valuation/valuation_ring): Value "group" is a group with zero (#17210)

kbuzzard committed 3 years ago

31b18ef9

feat(tactic/positivity): Extension for `function.const` (#17126)

YaelDillies committed 3 years ago

e3bf3f11