leanprover-community/mathlib3

Pull Requests Commits

refactor(linear_algebra/std_basis): remove std_basis

eric-wieser committed 3 years ago

693db66d

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

feat(number_theory/factorization): evaluating arithmetic functions at prime powers (#13817)

b-mehta committed 3 years ago

28031a80

feat(topology/vector_bundle): define some useful linear maps globally (#14484)

fpvandoorn committed 3 years ago

0575db0c

doc(set_theory/cardinal/cofinality): add myself as author (#14469)

vihdzp committed 3 years ago

c5f8d786

feat(category_theory/limits): is_kernel_of_comp (#14409)

TwoFX committed 3 years ago

4bd8c855

feat(linear_algebra/matrix): Spectral theorem for matrices (#14231)

abentkamp committed 3 years ago

29415900

feat(tactic/linear_combination): allow combinations of arbitrary proofs (#14229)

robertylewis committed 3 years ago

4e1eeebe

feat(topological_space/vector_bundle): reformulate linearity condition (#14485)

fpvandoorn committed 3 years ago

57885b4e

feat(tactic/linear_combination): allow arbitrary proof terms (#13979)

robertylewis committed 3 years ago

c414df7d

feat(order/conditionally_complete_lattice): Map `Inf` by monotone function (#14118)

vihdzp committed 3 years ago

12ad63e6

feat(order/filter/bases): view a filter as a *bundled* filter basis (#14506)

ADedecker committed 3 years ago

9600f4f6

refactor(topology/separation): rename `indistinguishable` to `inseparable` (#14401)

urkud committed 3 years ago

0950ba3d

Older