leanprover-community/mathlib3

Pull Requests Commits

adomani committed 3 years ago

9da7713c

adomani committed 3 years ago

ac52c1ab

feat(topology/continuous_function/zero_at_infty): add more instances for zero_at_infty_continuous_map and establish C₀ functorial properties (#13196)

j-loreaux committed 3 years ago

5e98dc1c

feat(category_theory/limits/shapes): isomorphisms of (co)spans (#13216)

kim-em committed 3 years ago

0719b36a

chore(algebra/associated): generalisation linter (#13108)

kim-em committed 3 years ago

b8971152

chore(algebra/order/{monoid,ring}): missing typeclasses about `*` and `+` on `order_dual` (#13004)

eric-wieser committed 3 years ago

cae51646

feat(analysis/normed_space/add_torsor_bases): add `convex.interior_nonempty_iff_affine_span_eq_top` (#13220)

urkud committed 3 years ago

02a25602

feat(data/polynomial/identities): golf using `linear_combination` (#13212)

hrmacbeth committed 3 years ago

0f4d0ae4

feat(number_theory/fermat4): golf using `linear_combination` (#13211)

hrmacbeth committed 3 years ago

3b04f48c

feat(algebra/quadratic_discriminant): golf using `linear_combination` (#13210)

hrmacbeth committed 3 years ago

82d1e9f8

refactor(category_theory/bicategory): set simp-normal form for 2-morphisms (#13185)

yuma-mizuno committed 3 years ago

4ff75f5b

feat(data/finset/basic): add `map_injective` and `sigma_equiv_option_of_inhabited` (#13083)

stuart-presnell committed 3 years ago

44c31d8f

feat(topology/metric/basic): construct a bornology from metric axioms and add it to the pseudo metric structure (#12078)

j-loreaux committed 3 years ago

9d786ce7

feat(data/nat/gcd): added gcd_mul_of_dvd_coprime (#12989)

seangolinski7 committed 3 years ago

2d2d09cb

chore(group_theory/index): Add `to_additive` (#13191)

tb65536 committed 3 years ago

733aed57

feat(data/polynomial/basic): add simp lemmas X_mul_C and X_pow_mul_C (#13163)

adomani committed 3 years ago

c522e3b5

feat(category_theory/monoidal): upgrades for monoidal equivalences (#13158)

kim-em committed 3 years ago

6a0524fd

feat(set_theory/cardinal): Upper bound on domain from upper bound on fibers (#13147)

tb65536 committed 3 years ago

d7ad7d37

feat(probability/integration): Bochner integral of the product of independent functions (#13140)

vbeffara committed 3 years ago

47a3cd26

feat(algebra/order/monoid): add eq_one_or_one_lt (#13131)

kbuzzard committed 3 years ago

ab1bf0fb

feat(group_theory/schreier): prove Schreier's lemma (#13019)

tb65536 committed 3 years ago

7c04f361

feat(archive/100-theorems-list/37_solution_of_cubic): golf (#13012)

hrmacbeth committed 3 years ago

315bff39

chore(order/symm_diff): Change the symmetric difference notation (#13217)

YaelDillies committed 3 years ago

c4f3869b

chore(algebra/char_p/{basic + algebra}): weaken assumptions for char_p_to_char_zero (#13214)

adomani committed 3 years ago

ac5188dd

feat(algebra/order/monoid): generalize, convert to `to_additive` and iff of `lt_or_lt_of_mul_lt_mul` (#13192)

adomani committed 3 years ago

321d159d

feat(order/monotone): simp lemmas for monotonicity in dual orders (#13207)

AntoineChambert-Loir committed 3 years ago

506ad313

feat(ring_theory/graded_algebra/homogeneous_localization): homogeneous localization ring is local (#13071)

jjaassoonn committed 3 years ago

be147af1

feat(order/symm_diff): More symmetric difference lemmas (#13133)

YaelDillies committed 3 years ago

3e4bf5de

chore(group_theory/index): Add `to_additive` (#13191)

tb65536 committed 3 years ago

faa7e52f

feat(data/polynomial/basic): add simp lemmas X_mul_C and X_pow_mul_C (#13163)

adomani committed 3 years ago

45a8f6cd

Older