leanprover-community/mathlib

Pull Requests Commits

feat(topology/continuous_map): lattice structures (#6706)

kim-em committed 4 years ago

87c12abd

chore(linear_algebra/finite_dimensional): change instance (#6713)

urkud committed 4 years ago

40a0ac77

feat(topology/separation): `(closure s).subsingleton ↔ s.subsingleton` (#6707)

urkud committed 4 years ago

177020e4

feat(measure_theory/measure_space): define `quasi_measure_preserving` (#6699)

urkud committed 4 years ago

890066ac

chore(*): update to Lean 3.28.0c (#6691)

bryangingechen committed 4 years ago

f5f42bc9

feat(geometry/manifold/mfderiv): more lemmas (#6679)

urkud committed 4 years ago

a116025e

feat(topology/algebra): more on closure (#6675)

kim-em committed 4 years ago

214b8e84

chore(ring_theory/noetherian): add `fg_span` and `fg_span_singleton` (#6709)

urkud committed 4 years ago

8d8c3560

feat(data/polynomial/degree/definitions): leading_coeff_X_pow_sub_C (#6633)

tb65536 committed 4 years ago

f221bfd8

feat(data/buffer/parser/*): expand parser properties (#6339)

pechersky committed 4 years ago

81dabdaf

chore(ring_theory/ideal): use `ideal.mul_mem_left` instead of `ideal.smul_mem` (#6704)

eric-wieser committed 4 years ago

03a6c95d

chore(geometry/manifold/times_cont_mdiff_map): add `times_cont_mdiff_map.mdifferentiable` (#6703)

urkud committed 4 years ago

d9fbe9d2

feat(algebra/iterate_hom): add `equiv.perm.coe_pow` (#6698)

urkud committed 4 years ago

ffacd120

refactor(topology/metric_space/emetric_space): add pseudo_emetric (#6694)

riccardobrasca committed 4 years ago

900963cd

feat(*): add some missing `coe_*` lemmas (#6697)

urkud committed 4 years ago

22eba86c

refactor(category_theory/limits): use auto_param (#6696)

kim-em committed 4 years ago

57de126a

feat(category/is_iso): make is_iso a Prop (#6662)

kim-em committed 4 years ago

c0036af2

feat(algebraic_topology/simplicial_object + ...): Add has_limits + has_colimits instances (#6695)

adamtopaz committed 4 years ago

6669a285

feat(topology): More lemmas from LTE, refactor `is_totally_disconnected` to use `set.subsingleton` (#6673)

PatrickMassot committed 4 years ago

6d7d1698

feat(ring_theory/finiteness): add `mv_polynomial_of_finite_presentation` (#6512)

riccardobrasca committed 4 years ago

0176b422

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

leanprover-community-bot committed 4 years ago

afe38ca1

feat(linear_algebra/quadratic_form): add nondegenerate_of_anisotropic (#6692)

kex-y committed 4 years ago

f1b69a12

refactor(topology/metric_space/isometry): move Kuratowski embedding to another file (#6678)

kim-em committed 4 years ago

ddb46177

feat(geometry/manifold/diffeomorph): expand API (#6668)

urkud committed 4 years ago

cc48a5a4

feat(measure_theory/outer_measure): golf, add lemmas (#6664)

urkud committed 4 years ago

bd386a8f

feat(meta/expr): monadic analogue of expr.replace (#6661)

kim-em committed 4 years ago

c358676b

feat(algebra/direct_sum_graded): a direct_sum formed of powers of a submodule of an algebra inherits a ring structure (#6550)

eric-wieser committed 4 years ago

3ec8c1d4

feat(algebra/free): turn `free_magma.lift` into an equivalence (#6672)

ocfnash committed 4 years ago

d9dc30e5

chore(geometry/manifold/times_cont_mdiff): add `prod_mk_space` versions of `prod_mk` lemmas (#6681)

urkud committed 4 years ago

ae776282

doc(readme): add Eric Wieser to maintainer list (#6688)

robertylewis committed 4 years ago

e16ae246

Newer Older