leanprover-community/mathlib3

Pull Requests Commits

chore(linear_algebra/exterior_algebra): Use a let to shorten the proof terms

eric-wieser committed 5 years ago

06088726

chore(linear_algebra/exterior_algebra): Avoid the unhelpful exterior_algebra.quot definition

eric-wieser committed 5 years ago

f44e6697

chore(linear_algebra/exterior_algebra): Use ring_quot

eric-wieser committed 5 years ago

63dffcae

chore(linear_algebra/exterior_algebra): Make the linter happy

eric-wieser committed 5 years ago

812e37ec

bug(linear_algebra/*): Fix sorry and remove duplicate lemma

eric-wieser committed 5 years ago

6857dc50

bug(linear_algebra/*): Update for changes to tensor_algebra

eric-wieser committed 5 years ago

9ffe7be1

bug(linear_algebra/*): Update for changes to `fin n`

eric-wieser committed 5 years ago

91b1778d

bug(ring_theory/algebra): Fix bad merge

eric-wieser committed 5 years ago

9b6a39aa

bug(group_theory/perm/sign): Tweak proofs to work on the latest lean/mathlib

eric-wieser committed 5 years ago

0ea5a75d

Merge remote-tracking branch 'origin/master' into exterior_algebra

eric-wieser committed 5 years ago

161a1028

chore(*): cleanup imports, split off data/finset/preimage from data/set/finite (#4221)

kim-em committed 5 years ago

5e934cd9

feat(data/mv_polynomial/rename): coeff_rename (#4203)

jcommelin committed 5 years ago

ed07cac5

feat(linear_algebra/eigenspace): generalized eigenvectors span the entire space (#4111)

abentkamp committed 5 years ago

ef18740b

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

leanprover-community-bot committed 5 years ago

4e414458

refactor(category_theory): make `has_image` and friends a Prop (#4195)

TwoFX committed 5 years ago

6b35819b

feat(data/(lazy_)list): various lemmas and definitions (#4172)

cipher1024 committed 5 years ago

96e81faa

feat(data/real/irrational): add a different formulation for irrationality (#4213)

jjaassoonn committed 5 years ago

69279580

feat(geometry/manifold): bundled smooth map (#3904)

Nicknamen committed 5 years ago

9aeffa83

feat(measure_theory): ext lemmas for measures (#3895)

fpvandoorn committed 5 years ago

72e5b9fc

fix(archive/100-thms): update link to 100.yaml in README (#4224)

bryangingechen committed 5 years ago

7cf8fa62

feat(data/polynomial/*): higher order derivative (#4187)

jjaassoonn committed 5 years ago

ecd889a5

feat(analysis/special_functions/trigonometric): continuity and differentiability of arctan (#4138)

hrmacbeth committed 5 years ago

5ab7eb0f

doc(data/list/tfae): Add skeletal docstring (#4220)

eric-wieser committed 5 years ago

d7aada16

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

leanprover-community-bot committed 5 years ago

937199ad

feat(archive/imo/*): add IMO 1972 B2, move IMOs to a subdirectory (#4209)

Stanislas Polu committed 5 years ago

392d3e37

feat(ring_theory/ideal/basic): mem_bot (#4211)

jcommelin committed 5 years ago

994c31d0

chore(data/mv_polynomial): Rename variables (#4208)

shingtaklam1324 committed 5 years ago

f2458d6f

refactor(ring_theory/algebra): re-bundle `subalgebra` (#4180)

Vierkantor committed 5 years ago

516b0dfd

feat(category_theory/monoidal): transport monoidal structure along an equivalence (#4123)

kim-em committed 5 years ago

d09ef4ab

feat(data/polynomial/degree/trailing_degree): basic definitions and properties (#4113)

adomani committed 5 years ago

caffd024

Older