leanprover-community/mathlib

Pull Requests Commits

feat(topology/order): upgrade some lemmas to `iff`s (#15617)

urkud committed 3 years ago

8ad82e4b

chore(analysis/normed/field/unit_ball): cleanup instances (#15615)

urkud committed 3 years ago

db107767

feat(topology/maps): add 2 lemmas, `open function` (#15612)

urkud committed 3 years ago

51891bef

feat(logic/equiv/local_equiv): add 2 lemmas (#15611)

urkud committed 3 years ago

1a73c7ee

feat(topology/algebra/module/finite_dimension): add 2 simp lemmas (#15610)

urkud committed 3 years ago

80d79069

chore(ring_theory/localization/basic): golf sec_snd_ne_zero (#15572)

Multramate committed 3 years ago

716616b3

chore(set_theory/ordinal/arithmetic): change `0 < x` assumptions to `x ≠ 0` (#15562)

vihdzp committed 3 years ago

4b82074e

feat(algebraic_geometry/AffineScheme): Affine communication lemma (#15487)

erdOne committed 3 years ago

ac9e3583

chore(set_theory/game/nim): review `simp` lemmas (#15407)

vihdzp committed 3 years ago

30edc932

feat(topology/instances/ennreal): add `continuous(_on).ennreal_mul` (#15593)

urkud committed 3 years ago

68451363

feat(data/set/intervals): add lemmas (#15608)

urkud committed 3 years ago

4d5ac734

feat(data/set/prod): add theorems about `λ x, (x, x)` (#15604)

urkud committed 3 years ago

98c62bd0

feat(integration): elementary version of FTC-1 (#15603)

PatrickMassot committed 3 years ago

e52026f7

chore(ring_theory/polynomial/symmetric): golf (#15598)

urkud committed 3 years ago

bd4a574f

Merge branch 'YK-isometry-lemmas' into YK-strict-convex-range

urkud committed 3 years ago

ae2e5404

docs(undergrad): add pointwise convergence (#15601)

PatrickMassot committed 3 years ago

e27e99b9

docs(undergrad): clean up distribution section (#15600)

PatrickMassot committed 3 years ago

2f99fd41

docs(undergrad): add polar integration (#15597)

PatrickMassot committed 3 years ago

d96fc102

refactor(data/list/chain): `transitive` → `is_trans` on `chain.pairwise` (#15571)

vihdzp committed 3 years ago

c97887bd

feat(analysis/calculus/cont_diff): generalize `mul` lemmas to a normed algebra (#15595)

urkud committed 3 years ago

d98479aa

urkud committed 3 years ago

e8a8fad7

doc(number_theory/bernoulli_polynomials): a few small improvements (#15599)

alexjbest committed 3 years ago

91416440

feat(order/succ_pred/limit): Successor and predecessor limits (#15001)

vihdzp committed 3 years ago

767aeb39

urkud committed 3 years ago

af70271f

feat(order/initial_seg): Initial/principal segment from empty type (#15375)

vihdzp committed 3 years ago

9bf23b0a

feat(data/real/basic): add a repr showing an underlying cauchy sequence (#15575)

eric-wieser committed 3 years ago

d749b205

feat(linear_algebra/linear_pmap): more lemmas about the graph (#15531)

mcdoll committed 3 years ago

c0c910de

urkud committed 3 years ago

e6346b62

feat(topology/metric_space/isometry): use `namespace`, add lemmas

urkud committed 3 years ago

88def16a

urkud committed 3 years ago

fda2009e

Newer Older