leanprover-community/mathlib3

Pull Requests Commits

feat(group_theory/subsemigroup/operations): port from submonoid (#12112)

pechersky committed 3 years ago

76de6f75

golf some ideal proofs

eric-wieser committed 3 years ago

bf2c3d71

chore(topology/continuous_function/continuous_map): add missing instances for `continuous_map` (#13717)

j-loreaux committed 3 years ago

560d1a71

refactor(number_theory/legendre_symbol/quadratic_reciprocity.lean): change definition of legendre_sym, simplify proofs, add lemmas (#13667)

MichaelStollBayreuth committed 3 years ago

325dbc88

feat(logic/relation): Transitive closure of well-founded relation is well-founded (#13698)

vihdzp committed 3 years ago

8b14d48f

Update src/algebra/module/submodule_bilinear.lean

eric-wieser committed 3 years ago

Verified 3bdaf2a5

doc(data/list/*): Fix file links (#13711)

YaelDillies committed 3 years ago

e77dbe0c

feat(analysis/normed_space/pointwise): The closure of a thickening (#13708)

YaelDillies committed 3 years ago

bfa0ba5b

feat(logic/relation): Add missing instances (#13704)

vihdzp committed 3 years ago

e6c6764d

feat(data/list/*): Miscellaneous lemmas (#13577)

YaelDillies committed 3 years ago

3d5e5ee1

feat(topology/order/priestley): Priestley spaces (#12044)

YaelDillies committed 3 years ago

c83488b9

feat(algebra/module/submodule_bilinear): add `submodule.map₂`, generalizing `submodule.has_mul`

eric-wieser committed 3 years ago

076419af

feat(algebra/module/linear_map) : cancel_right and cancel_left for linear_maps (#13703)

antoinelab01 committed 3 years ago

b0efdbbd

feat(set_theory/game/pgame): Conway induction on games (#13699)

vihdzp committed 3 years ago

5172448c

feat(group_theory/subgroup/basic): `zpowers_le` (#13693)

tb65536 committed 3 years ago

4c6b3737

refactor(linear_algebra/matrix/trace): unbundle `matrix.diag` (#13687)

eric-wieser committed 3 years ago

b94ea159

chore(tactic/field_simp): fix docstring (#13695)

sgouezel committed 3 years ago

6ae00ad3

feat(algebra/ring/equiv): generalize `ring_equiv` material to allow for non-unital rings (#13626)

j-loreaux committed 3 years ago

a02f11fa

feat(analysis/normed_space/pointwise): Thickening a thickening (#13380)

YaelDillies committed 3 years ago

1b1ae61f

feat(set_theory/game/pgame): `ordinal.to_pgame` (#13628)

vihdzp committed 3 years ago

093b583b

chore(scripts): update nolints.txt (#13706)

leanprover-community-bot committed 3 years ago

bf67d473

feat(order/filter/basic): more lemmas about `filter.comap` (#13619)

urkud committed 3 years ago

748ea79b

feat(algebra/ring/basic): define non-unital commutative (semi)rings (#13476)

j-loreaux committed 3 years ago

4de65278

feat(order/well-founded): Remove redundant arguments (#13702)

vihdzp committed 3 years ago

24a8bb93

feat(set_theory/cardinal/basic): Distributivity of `cardinal.sum` and + (#13643)

awainverse committed 3 years ago

438b39a7

feat(data/nat/totient): totient equals one iff (#13688)

ericrbg committed 3 years ago

8f604aa3

feat(category_theory/abelian): if D is abelian so is C ⥤ D (#13686)

kim-em committed 3 years ago

4e50b688

feat(data/fin/succ_pred): `fin` is an archimedean succ/pred order (#12792)

ericrbg committed 3 years ago

43e84cdd

feat(algebra/group_power/order): Add sq_zero_iff (#13670)

Smaug123 committed 3 years ago

4481a561

feat(analysis/normed_space/exponential): add `pi.exp_apply` (#13488)

eric-wieser committed 3 years ago

e2f56961

Newer Older