leanprover-community/mathlib3

Pull Requests Commits

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

feat(topology/metric_space): introduce `is_metric_separated` (#6685)

urkud committed 4 years ago

b5f38321

feat(analysis/calculus/times_cont_diff): smoothness of `f : E → Π i, F i` (#6674)

urkud committed 4 years ago

90db6fcc

feat(algebra/*, * : [regular, smul_with_zero, module/basic]): introduce `mul_action_with_zero` and `M`-regular elements (#6590)

adomani committed 4 years ago

1f47833e

feat(linear_algebra/quadratic_form): associated bilinear form over noncommutative rings (#6585)

hrmacbeth committed 4 years ago

abf2ab4d

refactor(data/polynomial,ring_theory): use big operators for polynomials (#6616)

gebner committed 4 years ago

249fd4f2

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

leanprover-community-bot committed 4 years ago

c5796c7b

feat(measure_theory/lp_space): add snorm_norm_rpow (#6619)

RemyDegenne committed 4 years ago

0a16148c

fix(algebra/continued_fractions): fix import (#6677)

kappelmann committed 4 years ago

feab14bc

feat(linear_algebra/alternating): Add dom_coprod (#5269)

eric-wieser committed 4 years ago

b48cf171

feat(topology/algebra/group): Add two easy lemmas (#6669)

PatrickMassot committed 4 years ago

b52337a5

feat(data/nat/fincard): introduce `nat.card`, `enat.card` (#6670)

awainverse committed 4 years ago

464d04af

chore(data/rat/basic): a few trivial lemmas about `rat.denom` (#6667)

urkud committed 4 years ago

70662e1c

feat(topology/basic): `f =ᶠ[𝓝 a] 0` iff `a ∉ closure (support f)` (#6665)

urkud committed 4 years ago

69d71341

feat(data/real/ennreal,topology/*): assorted lemmas (#6663)

urkud committed 4 years ago

c928e34d

refactor(ring_theory/discrete_valuation_ring): `discrete_valuation_ring.add_val` as an `add_valuation` (#6660)

awainverse committed 4 years ago

1e9f6646

feat(measure_theory/bochner_integration): extend the integral_smul lemmas (#6654)

RemyDegenne committed 4 years ago

d61d8bfe

Newer Older