leanprover-community/mathlib3

Pull Requests Commits

cut back changes:

eric-wieser committed 3 years ago

bf722019

Merge remote-tracking branch 'origin/master' into eric-wieser/bounded-computable

eric-wieser committed 3 years ago

f00f94fe

feat(ring_theory/graded_algebra/homogeneous_ideal): refactor `homogeneous_ideal` as a structure extending ideals (#12673)

jjaassoonn committed 3 years ago

d199eb99

feat(category_theory/monoidal): distribute tensor over direct sum (#12626)

kim-em committed 3 years ago

061d04b9

chore(category_theory/abelian/projective): fix typo (#12701)

jjaassoonn committed 3 years ago

078b213e

fix(category_theory/bicategory): remove spaces before closing parentheses (#12700)

yuma-mizuno committed 3 years ago

92e67597

chore(measure_theory): move and rename some lemmas (#12699)

urkud committed 3 years ago

0bd6dc2a

doc(data/equiv/encodable): +2 docstrings (#12698)

urkud committed 3 years ago

4b562f82

chore(cyclotomic/gal): update todo (#12693)

ericrbg committed 3 years ago

a3e0c85d

chore(algebra/module/basic): Move the scalar action earlier (#12690)

eric-wieser committed 3 years ago

77395f1e

feat(group_theory/abelianization): An application of the three subgroups lemma (#12677)

tb65536 committed 3 years ago

025fe7cb

chore(analysis/seminorm): Weaken typeclasses on `convex` and `locally_convex` lemmas (#12645)

mcdoll committed 3 years ago

b7978f39

feat(category_theory/preadditive) : definition of injective resolution (#12641)

jjaassoonn committed 3 years ago

53f6d687

refactor(linear_algebra/basic): split file (#12637)

kim-em committed 3 years ago

585d6419

feat(algebra/associated): add irreducible.not_dvd_one (#12686)

Ruben-VandeVelde committed 3 years ago

2ad9b39a

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

leanprover-community-bot committed 3 years ago

6d63c9be

feat(set_theory/ordinal_arithmetic): `smul` coincides with `mul` (#12692)

vihdzp committed 3 years ago

0fd9e309

feat(algebra/category): show categorical image in Module agrees with range (#12605)

kim-em committed 3 years ago

f3378562

chore(set_theory/ordinal_arithmetic): `well_founded` → `wf` (#12615)

vihdzp committed 3 years ago

11487179

feat(number_theory/function_field): add place at infinity (#12245)

mariainesdff committed 3 years ago

8d2e8871

feat(data/W/constructions): add constructions of W types (#12292)

Jlh18 committed 3 years ago

c1c61d44

chore(analysis/complex/upper_half_plane): don't use `abbreviation` (#12679)

urkud committed 3 years ago

2e562102

feat(tactic/interactive): guard_{hyp,target}_mod_implicit (#12668)

gebner committed 3 years ago

28775ced

feat(topology/separation): add t2_space_iff (#12628)

kbuzzard committed 3 years ago

d8ef1de0

feat(data/list/infix): add lemmas and instances (#12511)

astrainfinita committed 3 years ago

5242a7fb

refactor(data/set): generalize `set.restrict` and take set argument first in both `set.restrict` and `subtype.restrict` (#12510)

rish987 committed 3 years ago

df3792f8

feat(set_theory/ordinal_topology): Basic results on the order topology of ordinals (#11861)

vihdzp committed 3 years ago

c1edbec8

feat(data/finset/noncomm_prod): finite pi lemmas (#12291)

nomeata committed 3 years ago

09ea7fb0

chore(ci): update trepplein to version 1.1 (#12669)

gebner committed 3 years ago

fc882ff8

feat(set_theory/principal): If `a` isn't additive principal, it's the sum of two smaller ordinals (#12664)

vihdzp committed 3 years ago

abb8e5da

Older