leanprover-community/mathlib

Pull Requests Commits

awainverse committed 3 years ago

6534aad3

refactor(group_theory/commutator): Use variables and rearrange lemmas (#12629)

tb65536 committed 3 years ago

3da03b97

feat(category_theory/preadditive/Mat): ring version (#12617)

kim-em committed 3 years ago

23269bf0

feat(model_theory/definability): Definability with parameters (#12611)

awainverse committed 3 years ago

707df2cd

feat(algebra/category/Module): monoidal_preadditive (#12607)

kim-em committed 3 years ago

9293174a

feat(topology/algebra/continuous_monoid_hom): Define the Pontryagin dual (#12602)

tb65536 committed 3 years ago

e4ea2bca

feat(topology/category/Locale): The category of locales (#12580)

YaelDillies committed 3 years ago

5a9fb92b

feat(order/complete_lattice): add `complete_lattice.independent_pair` (#12565)

eric-wieser committed 3 years ago

96bae07c

chore(analysis/convex/strict): Reduce typeclass assumptions, golf (#12627)

YaelDillies committed 3 years ago

7e5ac6ad

feat(order/upper_lower): Upper/lower sets (#12189)

YaelDillies committed 3 years ago

22bdc8ec

chore(analysis): move lemmas around (#12621)

urkud committed 3 years ago

dc4e5cb4

chore(data/nat/prime): restate card_multiples without finset.sep (#12625)

Ruben-VandeVelde committed 3 years ago

7257ee71

chore(category_theory/closed/monoidal): fix notation (#12612)

kim-em committed 3 years ago

a63b99c3

chore(category_theory/limits): correct lemma names (#12606)

kim-em committed 3 years ago

956f3dbc

feat(group_theory/commutator): Prove `commutator_eq_bot_iff_le_centralizer` (#12598)

tb65536 committed 3 years ago

9456a744

feat(group_theory/subgroup/basic): add eq_one_of_noncomm_prod_eq_one_of_independent (#12525)

nomeata committed 3 years ago

b9ab27bd

split(analysis/locally_convex/basic): Split off `analysis.seminorm` (#12624)

YaelDillies committed 3 years ago

b21c1c9b

chore(algebra/category/Module): remove unnecessary universe restriction (#12610)

kim-em committed 3 years ago

a4187fef

fix(src/algebra/big_operators/multiset): unify prod_le_pow_card and prod_le_of_forall_le (#12589)

nomeata committed 3 years ago

31d28c62

feat(topology/homotopy): Homotopic maps induce naturally isomorphic functors between fundamental groupoid (#11595)

prakol16 committed 3 years ago

2241588b

doc(category_theory/monoidal/rigid): noting future work (#12620)

kim-em committed 3 years ago

5f3f70fe

refactor(group_theory/commutator): Golf proof of `commutator_mono` (#12619)

tb65536 committed 3 years ago

3d41a5bd

refactor(set_theory/ordinal_arithmetic): remove dot notation (#12614)

vihdzp committed 3 years ago

72c6979b

refactor(group_theory/commutator): Golf proof of `commutator_comm` (#12600)

tb65536 committed 3 years ago

3aaa5647

fix(tactic/suggest): fixing `library_search` (#12616)

arthurpaulino committed 3 years ago

1463f592

feat(analysis/inner_product_space/adjoint): gram lemmas (#12139)

hparshall committed 3 years ago

e8d0cacf

feat(group_theory/subgroup/basic): {multiset_,}noncomm_prod_mem (#12523)

nomeata committed 3 years ago

1eaf4999

feat(counterexample) : a homogeneous ideal that is not prime but homogeneously prime (#12485)

jjaassoonn committed 3 years ago

6ee6203c

refactor(group_theory/commutator): Move and golf `commutator_le` (#12599)

tb65536 committed 3 years ago

2e7483d2

chore({category_theory,order}/category/*): Missing `dsimp` lemmas (#12593)

YaelDillies committed 3 years ago

09d0f028

Older