leanprover-community/mathlib

Pull Requests Commits

urkud committed 3 years ago

da608488

Merge branch 'master' into YK-closure-arg

urkud committed 3 years ago

f087de55

feat(algebra/group/pi): add pi.nsmul_apply (#12122)

alexjbest committed 3 years ago

213e2ed7

feat(tactic/swap_var): name juggling, a weaker wlog (#12006)

pechersky committed 3 years ago

b3d09448

fix(category_theory/limits): improve inaccurate docstrings (#12130)

TwoFX committed 3 years ago

5f46dd09

feat(number_theory/divisors): add `prod_div_divisors` and `sum_div_divisors` (#12087)

stuart-presnell committed 3 years ago

7b6c4072

refactor(topology/metric_space/completion): change namespace (#12077)

urkud committed 3 years ago

33179f7e

feat(data/nat/fib): add that `fib` is sum of `nat.choose` along antidiagonal (#12063)

kmill committed 3 years ago

18c3e3f0

refactor(group_theory/abelianization): Define `commutator` in terms of `general_commutator` (#11949)

tb65536 committed 3 years ago

ffc2bdfb

refactor(ring_theory/fractional_ideal): rename lemmas for dot notation, add coe_pow (#12080)

eric-wieser committed 3 years ago

018c7289

feat(ring_theory/fractional_ideal): add coe_ideal lemmas (#12073)

mariainesdff committed 3 years ago

bcf8a6ed

feat(algebra/big_operators/intervals): summation by parts (#11814)

ecstatic-morse committed 3 years ago

98643bca

feat(data/equiv): define `ring_equiv_class` (#11977)

Vierkantor committed 3 years ago

3ca16d0a

chore(algebra/star/self_adjoint): extract a lemma from `has_scalar` (#12121)

eric-wieser committed 3 years ago

223f1496

doc(analysis/normed/group/basic): add docstring explaining the "insert" name (#12100)

eric-wieser committed 3 years ago

aed97e03

fix(category_theory/limits/shapes/images): make class a Prop (#12119)

jcommelin committed 3 years ago

3e6439cd

refactor(topology/algebra): reorder imports (#12089)

urkud committed 3 years ago

33b4e739

feat(data/finset/basic): add lemma `filter_eq_empty_iff` (#12104)

stuart-presnell committed 3 years ago

77f264f1

feat(algebra/indicator_function): smul lemmas for functions (#12059)

sgouezel committed 3 years ago

bb1b56c7

feat(topology/algebra): generalize `has_continuous_smul` arguments to `has_continuous_const_smul` (#11999)

eric-wieser committed 3 years ago

17b3357b

feat(linear_algebra/finite_dimensional): finrank_range_of_inj (#12067)

hparshall committed 3 years ago

b7572061

feat(data/finset/locally_finite): add Ico_subset_Ico_union_Ico (#11710)

BoltonBailey committed 3 years ago

59a183a1

feat(topology/instances/discrete): instances for the discrete topology (#11349)

RemyDegenne committed 3 years ago

e93996cf

feat(data/nat/totient): add Euler's product formula for totient function (#11332)

stuart-presnell committed 3 years ago

6089f08a

feat(analysis/inner_product_space/basic) : `inner_map_self_eq_zero` (#12065)

hparshall committed 3 years ago

19534b29

Revert "feat(category_theory/limits): is_bilimit"

TwoFX committed 3 years ago

8b6901b6

feat(category_theory/limits): is_bilimit

TwoFX committed 3 years ago

8edfa75d

feat(group_theory/commensurable): Definition and lemmas about commensurability. (#9545)

CBirkbeck committed 3 years ago

aacc36c5

feat(category_theory/limits): preservation of zero morphisms (#12068)

TwoFX committed 3 years ago

8575f592

chore(*): update to lean 3.39.2c (#12102)

gebner committed 3 years ago

c9e8c647

Older