leanprover-community/mathlib

Pull Requests Commits

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

prakol16 committed 4 years ago

2241588b

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

kim-em committed 4 years ago

5f3f70fe

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

tb65536 committed 4 years ago

3d41a5bd

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

vihdzp committed 4 years ago

72c6979b

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

tb65536 committed 4 years ago

3aaa5647

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

arthurpaulino committed 4 years ago

1463f592

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

hparshall committed 4 years ago

e8d0cacf

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

nomeata committed 4 years ago

1eaf4999

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

jjaassoonn committed 4 years ago

6ee6203c

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

tb65536 committed 4 years ago

2e7483d2

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

YaelDillies committed 4 years ago

09d0f028

feat(data/nat): add card_multiples (#12592)

Ruben-VandeVelde committed 4 years ago

4e302f54

feat(algebra/group/units_hom): make `is_unit.map` work on `monoid_hom_class` (#12577)

eric-wieser committed 4 years ago

222faeda

feat(category_theory): interderivability of kernel and equalizers in preadditive cats (#12576)

javra committed 4 years ago

8364980d

chore(*): update to 3.41.0c (#12591)

kmill committed 4 years ago

c0a51cf2

feat(algebra/module): add `module.nontrivial` (#12594)

urkud committed 4 years ago

e7db1936

feat(data/finset/noncomm_prod): add noncomm_prod_mul_distrib (#12524)

nomeata committed 4 years ago

5856c0c4

feat(set_theory/ordinal_arithmetic): Further theorems on normal functions (#12484)

vihdzp committed 4 years ago

dc5f7fbf

feat(data/list/prod_monoid): add prod_eq_pow_card (#12473)

nomeata committed 4 years ago

e3ad468b

feat(order/monotone): Folds of monotone functions are monotone (#12581)

vihdzp committed 4 years ago

7dcba96e

feat(linear_algebra/projective_space/basic): The projectivization of a vector space. (#12438)

adamtopaz committed 4 years ago

3dcc1689

feat(model_theory/substructures): Facts about substructures (#12258)

awainverse committed 4 years ago

003701f0

feat(set_theory/ordinal_arithmetic): The derivative of multiplication (#12202)

vihdzp committed 4 years ago

d6f337df

feat(algebra/order/monoid): add `with_zero.canonically_linear_ordered_add_monoid` (#12568)

eric-wieser committed 4 years ago

e6fef397

feat(order/sup_indep): add `finset.sup_indep_pair` (#12549)

eric-wieser committed 4 years ago

12786d04

chore(topology/algebra/module/basic): cleanup variables and coercions (#12542)

eric-wieser committed 4 years ago

4dc4dc8b

refactor(group_theory/commutator): Golf some proofs (#12586)

tb65536 committed 4 years ago

02e0ab2c

feat(order/hom): `prod.swap` as an `order_iso` (#12585)

urkud committed 4 years ago

d9a774e2

feat(data/list/basic): Miscellaneous `fold` lemmas (#12579)

vihdzp committed 4 years ago

840a0425

refactor(group_theory/solvable): Golf proof (#12552)

tb65536 committed 4 years ago

1a581ede

Newer Older