leanprover-community/mathlib3

Pull Requests Commits

feat(set_theory/game/nim): make the file `noncomputable theory` (#15367)

vihdzp committed 3 years ago

282da0c1

feat(order/upper_lower): Upper closure of a set (#15581)

YaelDillies committed 3 years ago

ab6bcd63

feat(data/polynomial/degree/definitions): redefine `polynomial.degree` as `p.support.max` (#15199)

adomani committed 3 years ago

1e024cb6

feat(analysis/locally_convex/with_seminorms): in a normed space, von Neumann bounded = metric bounded (#15124)

ADedecker committed 3 years ago

db22f697

move(order/{boolean_algebra → basic}): move `has_compl` and trivial instances (#15602)

vihdzp committed 3 years ago

b2ba27ce

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

urkud committed 3 years ago

0b1e039b

fix(data/json): `rbmap string α` never serializes to `null` (#15622)

eric-wieser committed 3 years ago

b93a64da

feat(order/boolean_algebra): A bounded generalized boolean algebra is a boolean algebra (#15606)

YaelDillies committed 3 years ago

81e26435

feat(data/set/function): add lemmas about `set.restrict` (#15605)

urkud committed 3 years ago

6b93ea7e

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

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

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

Newer Older