leanprover-community/mathlib

Pull Requests Commits

Try a `has_id` class too

Vierkantor committed 4 years ago

c434de12

"Fix" dot notation by introducing `⁻¹ₑ` and `⟪⟫ₑ` notation

Vierkantor committed 4 years ago

b23731f7

Don't forget to add your files :P

Vierkantor committed 4 years ago

5828e987

WIP: use bundled maps for `equiv.refl`,`equiv.symm`,`equiv.trans`

Vierkantor committed 4 years ago

753f17b7

Clarify comment

Vierkantor committed 4 years ago

Verified 0ca62502

Show `equiv_like.inv` is injective, like `coe`

Vierkantor committed 4 years ago

bf456200

Fix overlong line

Vierkantor committed 4 years ago

d7e9acec

feat(data/fun_like): define `embedding_like` and `equiv_like`

Vierkantor committed 4 years ago

a71e79e7

feat(category_theory/flat_functor): Generalize results into algebraic categories. (#10735)

erdOne committed 4 years ago

fcd0f11c

feat(data/nat/prime): add `prime.dvd_mul_of_dvd_ne` (#10727)

stuart-presnell committed 4 years ago

06905422

feat(algebra/{group,ring}/opposite): `{ring,monoid}_hom.from_opposite` (#10723)

eric-wieser committed 4 years ago

0c248b74

chore(algebra/module/submodule): missing is_central_scalar instance (#10720)

eric-wieser committed 4 years ago

4b079496

feat(algebra/tropical/big_operators): sum, prod, Inf (#10544)

pechersky committed 4 years ago

41def6a8

chore(linear_algebra/orientation): golf a proof (#10742)

eric-wieser committed 4 years ago

b9f24408

chore(tactic/reserved_notation): change precedence of sup and inf (#10623)

RemyDegenne committed 4 years ago

19dd4be3

refactor(data/{mv_,}polynomial): lemmas about `adjoin` (#10670)

urkud committed 4 years ago

61b0f419

move(data/bool/*): Move `bool` files in one folder (#10718)

YaelDillies committed 4 years ago

e68fcf8d

feat(algebra/order/ring): pos_iff_pos_of_mul_pos, neg_iff_neg_of_mul_pos (#10634)

jsm28 committed 4 years ago

50e318ec

chore(order/boolean_algebra): add `compl_sdiff` (#10722)

urkud committed 4 years ago

f3613738

feat(measure_theory): integral is mono in measure (#10721)

urkud committed 4 years ago

f9fff7c6

feat(group_theory/submonoid): The submonoid of left inverses of a submonoid (#10679)

erdOne committed 4 years ago

cc5ff8ca

feat(ring_theory/polynomial/cyclotomic/eval): `cyclotomic_pos` (#10482)

ericrbg committed 4 years ago

1c2b7420

refactor(algebra/group/basic): Migrate add_comm_group section into comm_group section (#10565)

mans0954 committed 4 years ago

f068b9de

Fix comment typo (#10715)

berndlosert committed 4 years ago

294753e9

feat(analysis/normed_space): normed space is homeomorphic to the unit ball (#10690)

urkud committed 4 years ago

97417665

chore(algebra/pointwise): Better `variables` management (#10686)

YaelDillies committed 4 years ago

08d30d66

feat(ring_theory/localization): Clearing denominators (#10668)

erdOne committed 4 years ago

d856bf9b

chore(algebra/group_with_zero/defs: Rename `comm_cancel_monoid_with_zero` to `cancel_comm_monoid_with_zero` (#10669)

YaelDillies committed 4 years ago

0b87b0ae

docs(topology/homotopy): add namespace in docstring to fix links (#10711)

ADedecker committed 4 years ago

52c2f742

feat(logic/function/basic): surjective function is an epimorphism (#10691)

urkud committed 4 years ago

a12fc705

Older