Commits leanprover-community/mathlib

fix(order/basic): fix `subtype.linear_order` (#15056)

urkud committed 3 years ago

9a2e5c8b

feat(category_theory): left-exact functors preserve finite limits (#14026)

javra committed 3 years ago

bbe25d4d

feat(combinatorics/simple_graph/regularity/equitabilise): Equitabilising a partition (#13222)

YaelDillies committed 3 years ago

d3f5adb0

feat(order/modular_lattice): Semimodular lattices (#11602)

YaelDillies committed 3 years ago

888caf7d

refactor(data/finite): move definition to a new file (#15204)

urkud committed 3 years ago

dfcbe856

data/multiset/range): add multiset.coe_range (#15201)

Ruben-VandeVelde committed 3 years ago

aae01cd3

chore(topology/basic): use `finite` in `locally_finite_of_finite` (#15181)

urkud committed 3 years ago

627bd0c2

feat(data/set/finite): add `multiset.finite_to_set` (#15177)

urkud committed 3 years ago

7f837db4

feat(linear_algebra): basis on R × R, and relation between matrices and linear maps in this basis (#15119)

sgouezel committed 3 years ago

ecd5234f

feat(analysis/inner_product_space): the Hellinger-Toeplitz theorem (#15055)

mcdoll committed 3 years ago

611dccaf

chore(topological_space/sober): use `namespace` and `variables`, golf (#15042)

urkud committed 3 years ago

0980bacb

feat(data/set/pointwise): `list` and `multiset` versions of n-ary lemmas (#14928)

eric-wieser committed 3 years ago

902e351c

feat(algebraic_geometry/projective_spectrum): forward direction of homeomorphism between top_space of Proj and top_space of Spec (#13397)

jjaassoonn committed 3 years ago

b7626956

chore(category_theory/adjunction/*): making arguments implicit in adjuction.comp and two small lemmas about mates (#15062)

Julian-Kuelshammer committed 3 years ago

cea27692

chore(algebra/order/ring): Normalize `_left`/`_right` (#14985)

YaelDillies committed 3 years ago

4e19dab9

feat(category_theory/endofunctor/algebra): Define coalgebras over an endofunctor and prove an equivalence (#14834)

Julian-Kuelshammer committed 3 years ago

40fdf72d

feat(category_theory/functor): preserving/reflecting monos/epis (#14829)

TwoFX committed 3 years ago

f7baecbb

feat(combinatorics/set_family/harris_kleitman): The Harris-Kleitman inequality (#14497)

YaelDillies committed 3 years ago

35363471

feat(order/bounded_order): Codisjointness (#14195)

YaelDillies committed 3 years ago

f5170fc5

feat(analysis/special_functions/pow): Rational powers are dense (#15002)

YaelDillies committed 3 years ago

b7148c4e

feat(data/nat/basic): split `exists_lt_and_lt_iff_not_dvd` into `if` and `iff` lemmas (#15099)

stuart-presnell committed 3 years ago

e3e4cc66

feat(algebra/category/BoolRing): The equivalence between Boolean rings and Boolean algebras (#15019)

YaelDillies committed 3 years ago

67779f73

refactor(data/finset/lattice): respell `finset.max/finset.min` using `sup/inf coe` (#15217)

adomani committed 3 years ago

b18b71c4

feat(category_theory/limits): opposites of limit pullback cones (#14526)

joelriou committed 3 years ago

ad080011

feat(set_theory/zfc): simp lemmas for `arity` and `const` (#15214)

vihdzp committed 3 years ago

f4f0f67b

feat(set_theory/zfc): basic lemmas on `pSet.equiv` (#15211)

vihdzp committed 3 years ago

cf4783fe

lint(topology/algebra/order/basic): use `finite` instead of `fintype` (#15203)

urkud committed 3 years ago

4b6ec60f

feat(algebra/order/monoid) Add zero_le_three and zero_le_four (#15219)

Multramate committed 3 years ago

f51aaab3

feat(data/finset/lattice): add three*2 lemmas about `finset.max/min` (#15212)

adomani committed 3 years ago

e5b8d09b

feat(data/pnat/basic): `succ` as an order isomorphism between `ℕ` and `ℕ+` (#15183)

vihdzp committed 3 years ago

5305d39a