leanprover-community/mathlib3

Pull Requests Commits

Added a @[symm]

awainverse committed 5 years ago

Verified 597994d4

Namespaced coprime

awainverse committed 5 years ago

2e3d0069

awainverse committed 5 years ago

492ca931

chore(analysis/normed_space): define `norm_one_class` (#4323)

urkud committed 5 years ago

48518578

feat(data/real/irrational): add a lemma to deduce nat_degree from irrational root (#4349)

jjaassoonn committed 5 years ago

d5834ee3

feat(archive/imo): formalize IMO 1969 problem 1 (#4261)

lacker committed 5 years ago

ddaa325e

feat(number_theory/divisors): defines the finsets of divisors/proper divisors, perfect numbers, etc. (#4310)

awainverse committed 5 years ago

7767ef8b

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

Older