leanprover-community/mathlib

Pull Requests Commits

feat(data/list/nodup): Add `list.nodup_iff` (#14371)

user7230724 committed 3 years ago

1f196cb2

doc(set_theory/ordinal/natural_ops): mention alternate names (#14546)

vihdzp committed 3 years ago

aa7d90bc

chore(order/bounded_order): move `order_dual` instances up, use them to golf lemmas (#14544)

urkud committed 3 years ago

8ef2c02c

refactor(topology): move code around (#14525)

urkud committed 3 years ago

50024528

perf(measure_theory/probability_mass_function/monad): speed up proof (#14519)

vihdzp committed 3 years ago

66b618d2

feat(data/int/basic): Units are either equal or negatives of each other (#14517)

tb65536 committed 3 years ago

3f26dfe2

feat(data/int/basic): Forward direction of `is_unit_iff_nat_abs_eq` (#14516)

tb65536 committed 3 years ago

b332507c

feat(analysis/special_functions): lemmas about filter `map`/`comap` (#14513)

urkud committed 3 years ago

2a9be5b5

feat(order/boolean_algebra, set/basic): some compl lemmas (#14508)

apnelson1 committed 3 years ago

0e943b15

feat(set_theory/ordinal/arithmetic): `has_exists_add_of_le` instance for `ordinal` (#14499)

vihdzp committed 3 years ago

27c4241b

feat(order/bounds): Bounds on `set.image2` (#14306)

YaelDillies committed 3 years ago

7c57af94

feat(order/conditionally_complete_lattice,data/real/nnreal): add 2 lemmas (#14545)

urkud committed 3 years ago

85fffda8

feat(data/multiset/basic): add some lemmas (#14421)

Ruben-VandeVelde committed 3 years ago

72ac40e9

chore(set_theory/surreal/basic): golf (#14168)

vihdzp committed 3 years ago

a418945a

feat(set_theory/game/pgame): Add dot notation on many lemmas (#14149)

vihdzp committed 3 years ago

e1b3351d

feat(set_theory/ordinal/natural_ops): define natural addition (#14291)

vihdzp committed 3 years ago

00982865

feat(analysis/calculus/fderiv_measurable): the right derivative is measurable (#14527)

sgouezel committed 3 years ago

d63246c0

refactor(algebra/order/ring): turn `sq_le_sq` into an `iff` (#14511)

urkud committed 3 years ago

2a21a861

docs(order/boolean_algebra): typo in generalized boolean algebra doc (#14536)

apnelson1 committed 3 years ago

fa226034

feat(measure_theory/integral/lebesgue): approximate a function by a finite integral function in a sigma-finite measure space. (#14528)

sgouezel committed 3 years ago

6ca5910f

feat(analysis/calculus/tangent_cone): unique differentiability of open interval at endpoint (#14530)

sgouezel committed 3 years ago

bec8b65e

feat(algebra/char_zero): add a lemma `ring_hom.injective_nat` (#14414)

astrainfinita committed 3 years ago

705160e9

feat(data/polynomial/eval): reduce assumptions, add a lemma (#14391)

astrainfinita committed 3 years ago

d2dcb74a

feat(topology/algebra/module/finite_dimension): all linear maps from a finite dimensional T2 TVS are continuous (#13460)

ADedecker committed 3 years ago

c9d69a46

feat(linear_algebra/basis): repr_support_of_mem_span (#14504)

abentkamp committed 3 years ago

31cbfbb0

feat(analysis/complex/upper_half_plane): extend action on upper half plane to GL_pos (#12415)

hrmacbeth committed 3 years ago

2b69bb43

feat(data/nat/basic): add lemmas about `nat.bit_cases_on` (#14481)

urkud committed 3 years ago

1a1895cd

feat(data/int/basic): Lemmas for when a square equals 1 (#14501)

tb65536 committed 3 years ago

ade30c34

refactor(field_theory/normal): generalize `lift_normal` and `restrict_normal` (#14450)

isadofschi committed 3 years ago

e4433311

refactor(data/set/finite): protect `set.finite` (#14344)

kmill committed 3 years ago

ae025835

Newer Older