leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 3 years ago

5f38113e

Merge remote-tracking branch 'origin/master' into function_field

eric-wieser committed 3 years ago

03c1a85a

feat(algebra/group/to_additive): let to_additive turn `pow` into `nsmul` (#12477)

nomeata committed 3 years ago

eb46e7e3

refactor(set_theory/*): `o.out.r` → `<` (#12468)

vihdzp committed 3 years ago

d704f27e

feat(analysis/normed/group/hom): add a module instance (#12465)

eric-wieser committed 3 years ago

9dd8ec1e

feat(measure_theory/group/arithmetic): actions by int and nat are measurable (#12464)

eric-wieser committed 3 years ago

0b86bb8d

feat(data/nat/basic): add one_le_div_iff (#12461)

kbuzzard committed 3 years ago

3f353db2

feat(measure_theory/constructions/polish): injective images of Borel sets in Polish spaces are Borel (#12448)

sgouezel committed 3 years ago

2675b5c3

feat(set_theory/ordinal_arithmetic): `enum_ord univ = id` (#12391)

vihdzp committed 3 years ago

37783539

feat(category_theory/*): preserves biproducts implies additive (#12014)

TwoFX committed 3 years ago

313f4055

feat(geometry/manifold/tangent_bundle): the `tangent_bundle` is a `topological_vector_bundle` (#8295)

Nicknamen committed 3 years ago

f063d0c6

doc(algebra/group/to_additive): `to_additive` and docstring interaction (#12476)

nomeata committed 3 years ago

a19f6c6f

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

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

Older