leanprover-community/mathlib

Pull Requests Commits

awainverse committed 3 years ago

63de07c5

awainverse committed 3 years ago

032df4fe

refactor(analysis/complex): replace `diff_on_int_cont` with `diff_cont_on_cl` (#13148)

urkud committed 3 years ago

cc65716e

feat(order/bounds): Boundedness of monotone/antitone functions (#13079)

MantasBaksys committed 3 years ago

57f382a0

feat(data/list/chain): Lemma for `chain r a (list.range n.succ)` (#12990)

vihdzp committed 3 years ago

0dde2cb8

feat(data/polynomial/degree/lemmas): add some lemmas and rename some lemmas (#13235)

astrainfinita committed 3 years ago

bc140d29

feat(data/polynomial/eval): add some lemmas for `eval₂` (#13234)

astrainfinita committed 3 years ago

f8467aaf

feat(group_theory/schreier): Add version of Schreier's lemma (#13231)

tb65536 committed 3 years ago

25d28c83

feat(computability/encoding): Bounds on cardinality from an encoding (#13224)

awainverse committed 3 years ago

d831478d

feat(category_theory/bicategory): monoidal categories are single object bicategories (#13157)

kim-em committed 3 years ago

6abb6de9

feat(linear_algebra/general_linear_group): Add some lemmas about SL to GL_pos coercions. (#12393)

CBirkbeck committed 3 years ago

823699fb

chore(algebra/associated): golf irreducible_iff_prime_iff (#13267)

Ruben-VandeVelde committed 3 years ago

d42f6a82

chore(archive/imo/imo1994_q1): tidy a bit (#13266)

Ruben-VandeVelde committed 3 years ago

348b41d4

chore(algebraic_geometry/pullbacks): replaced some simps by simp onlys (#13258)

arthurpaulino committed 3 years ago

1d9d1530

feat(group_theory/commutator): The commutator subgroup is characteristic (#13255)

tb65536 committed 3 years ago

8c7e8a4d

refactor(group_theory/solvable): Golf and move `solvable_of_ker_le_range` (#13254)

tb65536 committed 3 years ago

d23fd6f7

refactor(group_theory/solvable): Golf some proofs (#13256)

tb65536 committed 3 years ago

f24918e0

feat(category_theory/faithful): map_iso_injective (#13263)

kim-em committed 3 years ago

d6ff44ec

feat(data/nat/*): generalize typeclass assumptions (#13260)

ericrbg committed 3 years ago

7a0513db

feat(category_theory/triangulated): upgrade map_triangle to a functor (#13262)

kim-em committed 3 years ago

f5ee47b6

chore(measure_theory): move lemmas about `ae_measurable` to a new file (#13246)

urkud committed 3 years ago

a98a26b2

chore(analysis/special_functions/pow): golf a proof (#13247)

urkud committed 3 years ago

59cf3675

feat(data/list/big_operators): More lemmas about alternating product (#13195)

YaelDillies committed 3 years ago

2a04ec03

feat(algebra/big_operators): some big operator lemmas (#13066)

Vierkantor committed 3 years ago

485d6484

awainverse committed 3 years ago

97e88eee

feat(group_theory/group_action/fixing_subgroup): add lemmas about fixing_subgroup (#13202)

AntoineChambert-Loir committed 3 years ago

9498beac

feat(category_theory/limits/terminal): limit of the constant terminal functor (#13238)

kim-em committed 3 years ago

ed266e51

feat(category_theory/limits/pullbacks): missing simp lemmas (#13237)

kim-em committed 3 years ago

afa9be28

feat(analysis/locally_convex/basic): add lemmas about finite unions for absorbs (#13236)

mcdoll committed 3 years ago

05213440

feat(data/polynomial/degree/definitions): add `degree_monoid_hom` (#13233)

astrainfinita committed 3 years ago

0831e4f1

Older