leanprover-community/mathlib

Pull Requests Commits

feat(order/symm_diff): Heyting bi-implication (#16544)

YaelDillies committed 4 years ago

8cd94b84

chore(tactic/{core + compute_degree}): tightening up compute_degree_le (#15649)

adomani committed 4 years ago

2d915e4e

feat(data/complex/basic): bundle complex.abs (#16347)

ericrbg committed 4 years ago

ba80091d

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

leanprover-community-bot committed 4 years ago

5947fb69

chore(linear_algebra/matrix/adjugate): remove unnecessary fin_cases with (#16605)

kim-em committed 4 years ago

44eb23a5

chore(data/finset/basic): Scope variables over smaller sections (#16613)

eric-wieser committed 4 years ago

ac01c538

feat(algebra/punit_instances): linear_ordered_add_comm_monoid_with_top punit (#16609)

ericrbg committed 4 years ago

27b90386

chore(docs): run `bibtool` on `references.bib` (#16606)

eric-wieser committed 4 years ago

01894cc4

feat(topology/separation): connected sets in a t1 space are infinite (#16584)

ericrbg committed 4 years ago

8deb2a68

doc(group_theory/sylow): update docstring to include card_eq_multiplicity as a main result (#14354)

ChrisHughes24 committed 4 years ago

e1783b0f

feat(group_theory/group_action): define `distrib_smul` and `smul_zero_class` (#16123)

Vierkantor committed 4 years ago

8f66240c

feat(category_theory/limits/shapes/biproducts): more (co)kernel instances (#14188)

kim-em committed 4 years ago

249a9c91

feat(order/filter/lift): replace some implications with iffs (#16452)

urkud committed 4 years ago

313f36d4

chore(data/finset/basic): move `disjoint` proofs earlier (#16436)

eric-wieser committed 4 years ago

24b50bfc

feat(analysis/normed_space/affine_isometry): `subtypeₐᵢ` (#16573)

jsm28 committed 4 years ago

d0507e7b

chore(tactic): typos in docs (#16510)

kim-em committed 4 years ago

f89fa08b

feat(topology/subset_properties): an infinite type with cofinite topology is irreducible (#16499)

urkud committed 4 years ago

02022cd6

feat(analysis/special_functions/pow, set_theory/*): `positivity` extension for powers (#16462)

YaelDillies committed 4 years ago

53322d0d

chore(category/endomorphism): remove unneeded ext attribute (#16603)

kim-em committed 4 years ago

028afe5d

chore(topology/basic): rename lemmas (#16598)

astrainfinita committed 4 years ago

39723052

chore(.github/workflows): `maintainer merge` workflow (#16555)

jcommelin committed 4 years ago

79a2eb39

chore(tactic/monotonicity/lemmas): Move lemmas to the correct places (#16509)

YaelDillies committed 4 years ago

98cbfb45

chore(analysis): golf a few proofs (#16600)

mcdoll committed 4 years ago

33075a02

doc(topology/algebra/filter_basis): modify doc of `add_group_filter_basis_of_comm` (#16597)

faenuccio committed 4 years ago

9806b5c3

chore(topology): golf (#16585)

urkud committed 4 years ago

1732f9cf

feat(set_theory/game/nim): recursors for left/right nim moves (#15408)

vihdzp committed 4 years ago

f18afbe9

refactor(data/set/basic): Remove _eq lemmas (#16572)

wrenna-robson committed 4 years ago

951bf1d9

feat(tactic/positivity): Extension for `coe` (#16141)

YaelDillies committed 4 years ago

3dc8592b

feat(geometry/manifold/instances/sphere): the differential of the embedding of the sphere into its ambient space (#16466)

hrmacbeth committed 4 years ago

69071436

feat(probability/martingale/centering): uniqueness of Doob's decomposition (#16532)

kex-y committed 4 years ago

e18fa7b9

Newer Older