leanprover-community/mathlib

Pull Requests Commits

refactor(ring_theory/perfection): faster proof of `coeff_frobenius`

Jesse Michael Han committed 4 years ago

74e23d34

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

leanprover-community-bot committed 4 years ago

69bf4840

chore(linear_algebra/basic, analysis/normed_space/operator_norm): bundle another argument into the homs (#5899)

eric-wieser committed 4 years ago

117e7290

feat(analysis/normed_space): `continuous_linear_map.prod` as a `linear_isometry_equiv` (#6099)

urkud committed 4 years ago

7f11d721

doc(algebra/{field_power, punit_instances}): module docs (#6097)

Julian-Kuelshammer committed 4 years ago

03074b12

feat(differential_object/iso_app): extract the isomorphism of underlying objects (#6083)

kim-em committed 4 years ago

d62d7937

feat(linear_algebra/basis): if `(p : submodule K V) < ⊤`, then there exists `f : V →ₗ[K] K`, `p ≤ ker f` (#6074)

urkud committed 4 years ago

0c6fa288

feat(measure_theory/probability_mass_function): Add definitions for filtering pmfs on a predicate (#6033)

dtumad committed 4 years ago

4e9fbb94

feat(computability/DFA): the pumping lemma (#5925)

foxthomson committed 4 years ago

f6504f1a

chore(data/finset): golf some proofs (#6101)

kim-em committed 4 years ago

1d49f87e

feat(linear_algebra/basic): bundle prod and coprod into linear_equivs (#5992)

eric-wieser committed 4 years ago

1a0f84c7

feat(topology/instances/{nnreal,ennreal}): add tendsto_cofinite_zero_of_summable (#6093)

RemyDegenne committed 4 years ago

8a23aa3b

feat(category_theory/pi): extract components of isomorphisms of indexed objects (#6086)

kim-em committed 4 years ago

8e3e79a2

feat(category_theory/differential_object): lifting a functor (#6084)

kim-em committed 4 years ago

f075a698

feat(topology/local_extr): not locally surjective at a local extr (#6076)

urkud committed 4 years ago

65616390

feat(analysis/calculus): derivatives of `f : E → Π i, F i` (#6075)

urkud committed 4 years ago

054b4676

feat(linear_algebra/pi_tensor_product): add reindex and pempty_equiv (#6069)

eric-wieser committed 4 years ago

dc48a849

feat(norm_cast): dite_cast to match ite_cast (#6092)

kim-em committed 4 years ago

d7a4f727

feat(topology/constructions): a finite product of discrete spaces is discrete (#6088)

kim-em committed 4 years ago

b338240e

chore(algebra/module/prod): add missing instances (#6055)

eric-wieser committed 4 years ago

e4369fe3

feat(topology/continuous_map): missing coe_mk lemma (#6087)

kim-em committed 4 years ago

90702a04

feat(finset/lattice): max'_insert (#6089)

kim-em committed 4 years ago

a6fc6bdc

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

leanprover-community-bot committed 4 years ago

6b83e728

chore(analysis/calculus/local_extr): review (#6085)

urkud committed 4 years ago

5bf92e1d

feat(topology/separation): an injective map on a compact space is an embedding (#6057)

sgouezel committed 4 years ago

45f95448

feat(algebra/lie/basic): define the center of a Lie algebra and prove some related results (#6013)

ocfnash committed 4 years ago

9411b00e

feat(measure_theory/lebesgue_measure): integral as volume between graphs (#5932)

asouther4 committed 4 years ago

d989ff47

chore(measure_theory): use `∞` notation for `(⊤ : ℝ≥0∞)` (#6080)

urkud committed 4 years ago

f3b0295a

feat(analysis): prove that a polynomial function is equivalent to its leading term along at_top, and consequences (#5354)

ADedecker committed 4 years ago

5d4d8158

refactor(measure_theory/ae_eq_fun): move emetric to `ae_eq_fun_metric` (#6081)

sgouezel committed 4 years ago

99fe12af

Older