Commits leanprover-community/mathlib

chore(set_theory/ordinal_arithmetic): Golf `lsub_typein` and `blsub_id` (#12203)

vihdzp committed 3 years ago

b7808a99

feat(category_theory/limits): transport is_limit along F.left_op and similar (#12166)

TwoFX committed 3 years ago

b4d007fc

feal(category_theory/bicategory/functor): define pseudofunctors (#11992)

yuma-mizuno committed 3 years ago

371b48a0

feat(category_theory/limits): uniqueness of preadditive structures (#12342)

TwoFX committed 3 years ago

62e7d353

Merge branch 'master' of https://github.com/leanprover-community/mathlib

jjaassoonn committed 3 years ago

9647e5bd

feat(data/polynomial/monic): add monic_of_mul_monic_left/right (#12446)

alexjbest committed 3 years ago

974d23c2

feat(category_theory/full_subcategory): full_subcategory.map and full_subcategory.lift (#12335)

TwoFX committed 3 years ago

e542154b

feat(model_theory/terms_and_formulas): Using a list encoding, bounds the number of terms (#12276)

awainverse committed 3 years ago

51adf3a1

feat(category_theory/discrete_category): generalize universes for comp_nat_iso_discrete (#12340)

TwoFX committed 3 years ago

92b27e12

feat(category_theory/abelian): faithful functors reflect exact sequences (#12071)

TwoFX committed 3 years ago

4ecd92a9

feat(data/nat/prime): add nat.eq_two_pow_or_exists_odd_prime_and_dvd (#12395)

Ruben-VandeVelde committed 3 years ago

fa6b16e1

feat(order/hom/basic): add `order_iso.with_{top,bot}_congr` (#12264)

eric-wieser committed 3 years ago

8b913902

doc(topology/uniform_space/cauchy): fix typo (#12453)

mcdoll committed 3 years ago

2840532e

golf

jjaassoonn committed 3 years ago

70a3ba86

golf

jjaassoonn committed 3 years ago

f5198ce7

feat(category_theory/abelian/exact): `exact g.op f.op`

jjaassoonn committed 3 years ago

ff59ac8f

feat(measure_theory/card_measurable_space): cardinality of generated sigma-algebras (#12422)

sgouezel committed 3 years ago

bda091dd

feat(order/category/BoolAlg): The category of Boolean algebras (#12452)

YaelDillies committed 3 years ago

93451afd

feat(linear_algebra/clifford_algebra/conjugation): reverse and involute are grade-preserving (#12373)

eric-wieser committed 3 years ago

f5b885b0

feat(data/nat/fib): add bit0/bit1 lemmas and fast_fib (#12444)

kmill committed 3 years ago

ac28ddf7

feat(set_theory/ordinal_arithmetic): `add_le_of_forall_add_lt` (#12315)

vihdzp committed 3 years ago

36a528d1

feat(category_theory/preadditive/injective) : more basic properties and morphisms about injective objects (#12450)

jjaassoonn committed 3 years ago

b0d94624

feat(category_theory/closed): generalize some material from cartesian closed categories to closed monoidal categories (#12386)

kim-em committed 3 years ago

fdf43f1c

feat(analysis/normed_space/star/matrix): `entrywise_sup_norm_bound_of_unitary` (#12255)

hparshall committed 3 years ago

45d235e8

feat(topology/compacts): The types of clopens and of compact opens (#11966)

YaelDillies committed 3 years ago

17559112

feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative (#12231)

dupuisf committed 3 years ago

8e1da4e6

feat(order/category/Frame): The category of frames (#12363)

YaelDillies committed 3 years ago

3ac971be

feat(ring_theory/simple_module): Simple modules as simple objects in the Module category (#11927)

pbazin committed 3 years ago

ee4be2db

feat(ring_theory/polynomial/homogeneous) : add lemma `homogeneous_component_homogeneous_polynomial` (#10113)

jjaassoonn committed 3 years ago

a07cf6bd

feat(topology/algebra/weak_dual): generalize to weak topologies for arbitrary dualities (#12284)

mcdoll committed 3 years ago

34d8ff1d