leanprover-community/mathlib

Pull Requests Commits

Fix merge issues

eric-wieser committed 5 years ago

5939388c

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

eric-wieser committed 5 years ago

85df37ce

feat(data/nat/basic): simp-lemmas for bit0 and bit1 mod two (#4343)

jcommelin committed 5 years ago

f10dda05

feat(data/mv_polynomial): stub on invertible elements (#4320)

robertylewis committed 5 years ago

0fc7b29e

feat(linear_algebra): determinant of `matrix.block_diagonal` (#4300)

Vierkantor committed 5 years ago

3d58fce5

feat(linear_algebra/exterior_algebra): Add an exterior algebra (#4297)

eric-wieser committed 5 years ago

13e9cc4a

feat(geometry/manifold): derivative of the zero section of the tangent bundle (#4292)

sgouezel committed 5 years ago

268073ae

feat(data/polynomial/*) : as_sum_support (#4286)

jjaassoonn committed 5 years ago

11cdc8cf

feat(data/nat/fact, analysis/specific_limits): rename nat.fact, add few lemmas about its behaviour along at_top (#4309)

ADedecker committed 5 years ago

0ccc1573

feat(*): a few more tests for `summable`, docstrings (#4325)

urkud committed 5 years ago

9c241b0d

feat(algebra/ordered_ring): ask for 0 < 1 earlier. (#4296)

kim-em committed 5 years ago

fb2b1de0

feat(analysis/normed_space/inner_product): Define the inner product based on `is_R_or_C` (#4057)

dupuisf committed 5 years ago

9ceb1141

feat(data/fintype): pigeonhole principles (#4096)

kmill committed 5 years ago

1b973263

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

leanprover-community-bot committed 5 years ago

af994169

feat(geometry/manifold): smooth bundled maps (#3641)

Nicknamen committed 5 years ago

bcc7c024

feat(archive/imo): formalize IMO 1959 problem 1 (#4340)

lacker committed 5 years ago

c04e3398

chore(ring_theory/algebra): Mark algebra.mem_top as simp (#4339)

eric-wieser committed 5 years ago

23b04b0f

feat(analysis/convex): slope_mono_adjacent (#4307)

MaloJaffre committed 5 years ago

decd67c4

chore(*): Tidy some proofs and variables (#4338)

eric-wieser committed 5 years ago

a06c87ed

fix(ring_theory/algebra): Fix typo "algbera" (#4337)

eric-wieser committed 5 years ago

9921fe71

feat(ring_theory/algebra): some lemmas about numerals in algebras (#4327)

kim-em committed 5 years ago

05038da0

chore(*): rename is_unit_pow to is_unit.pow (#4329)

jcommelin committed 5 years ago

5fd2037e

feat(topology/bounded_continuous_function): normed_comm_ring structure on bounded continuous functions (#4326)

hrmacbeth committed 5 years ago

ac797ad5

feat(order/basic): lemmas about `strict_mono_incr_on` (#4313)

urkud committed 5 years ago

e53aa870

feat(ring_theory/jacobson): Integral extension of Jacobson rings are Jacobson (#4304)

dtumad committed 5 years ago

e1c0b0a9

chore(category_theory/limits): facts about opposites of limit cones (#4250)

kim-em committed 5 years ago

ff66d924

feat(*): preparations for roots of unity (#4322)

jcommelin committed 5 years ago

da66bb81

feat(algebra/pointwise): Add missing to_additive on finset lemmas (#4306)

eric-wieser committed 5 years ago

743f82ca

feat(data/prod): mk injective lemmas (#4319)

robertylewis committed 5 years ago

669a3499

feat(algebra/invertible): invertible.copy (#4318)

robertylewis committed 5 years ago

d301d431

Older