leanprover-community/mathlib3

Pull Requests Commits

jcommelin committed 3 years ago

2f4ab663

eric-wieser committed 3 years ago

324acfae

Merge branch 'jjaassoonn/counter_example_prime_not_hom_prime' of https://github.com/leanprover-community/mathlib into jjaassoonn/counter_example_prime_not_hom_prime

jjaassoonn committed 3 years ago

5ef5d255

jjaassoonn committed 3 years ago

0d65d300

Update opposite.lean

jjaassoonn committed 3 years ago

Verified 9f4c1d00

Update exact.lean

jjaassoonn committed 3 years ago

Verified d467b255

jjaassoonn committed 3 years ago

6a79e8a0

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

jjaassoonn committed 3 years ago

71ccc1fc

feat(ring_theory/graded_algebra/radical) : radical of homogeneous ideal is homogeneous (#12277)

jjaassoonn committed 3 years ago

92ef3c51

chore(set_theory/cardinal_divisibility): add instance unique (units cardinal) (#12458)

Ruben-VandeVelde committed 3 years ago

40602e65

chore(set_theory/ordinal_arithmetic): Reorder theorems (#12475)

vihdzp committed 3 years ago

66961879

feat(analysis/normed_space/star/spectrum): prove the spectral radius of a star normal element is its norm (#12249)

j-loreaux committed 3 years ago

0a6efe0f

fix(algebra/group/pi): Fix apply-simp-lemmas for monoid_hom.single (#12474)

nomeata committed 3 years ago

28c902d8

refactor(set_theory/ordinal): `enum_lt` → `enum_lt_enum` (#12469)

vihdzp committed 3 years ago

64d953a1

feat(category_theory/abelian): (co)kernels in terms of exact sequences (#12460)

TwoFX committed 3 years ago

d61ebab1

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

jjaassoonn committed 3 years ago

70a3ba86

jjaassoonn committed 3 years ago

f5198ce7

Older