leanprover-community/mathlib3

Pull Requests Commits

hrmacbeth committed 4 years ago

590e4430

feat(data/list/cycle): cycles as quotients of lists (#7504)

pechersky committed 4 years ago

a564bf1e

refactor(geometry/manifold/instances/circle): split out (topological) group facts (#7951)

hrmacbeth committed 4 years ago

0490b432

chore(measure_theory/lp_space): simplify tendsto_Lp_iff_tendsto_\McLp by using tendsto_iff_dist_tendsto_zero (#7942)

RemyDegenne committed 4 years ago

95a116a1

refactor(algebra/algebra/basic): replace `algebra.comap` with `restrict_scalars` (#7949)

hrmacbeth committed 4 years ago

690ab173

feat(algebraic_geometry/Spec): Make Spec a functor. (#7790)

justus-springer committed 4 years ago

b8658928

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

leanprover-community-bot committed 4 years ago

ba3a4b7a

fix(measure_theory/interval_integral): generalize some lemmas (#7944)

benjamindavidson committed 4 years ago

30314c22

feat(order/iterate): id_le lemmas (#7943)

YaelDillies committed 4 years ago

45619c73

feat(analysis/convex/basic): a linear map is convex and concave (#7934)

YaelDillies committed 4 years ago

e5c97e10

feat(analysis/convex/basic): convex_on lemmas (#7933)

YaelDillies committed 4 years ago

f1f4c23f

feat(analysis/normed_space/dual): add eq_zero_of_forall_dual_eq_zero (#7929)

RemyDegenne committed 4 years ago

5d03dcd4

feat(data/finsupp/basic): equiv_congr_left (#7755)

digama0 committed 4 years ago

e5ff5fb4

feat(measure_theory/lp_space): add `mem_Lp.mono_measure` (#7927)

RemyDegenne committed 4 years ago

2f1f34a9

docs(undergrad): mark convex, convex hull, and extreme points as done (#7924)

YaelDillies committed 4 years ago

5f8cc8eb

feat(group_theory/order_of_element): Raising to a coprime power is a bijection (#7923)

tb65536 committed 4 years ago

e4ceee66

feat(measure_theory/bochner_integration): properties of simple functions (mem_Lp, integrable, fin_meas_supp) (#7918)

RemyDegenne committed 4 years ago

f4991b97

chore(order/lattice): rename le_sup_left_of_le (#7856)

YaelDillies committed 4 years ago

b19c491a

feat(algebra/algebra/basic): define `restrict_scalars.linear_equiv` (#7807)

ocfnash committed 4 years ago

8e281044

feat(geometry/manifold/algebra/smooth_functions): add `coe_fn_(linear_map|ring_hom|alg_hom)` (#7749)

Nicknamen committed 4 years ago

a16650c4

chore(algebra/{ordered_monoid_lemmas, ordered_monoid}): move two sections close together (#7921)

adomani committed 4 years ago

bf83c301

fix(meta/expr): fix mreplace (#7912)

fpvandoorn committed 4 years ago

d74a8989

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

leanprover-community-bot committed 4 years ago

d960b2d8

chore(topology/metric_space): cleanup Gromov-Hausdorff files (#7936)

sgouezel committed 4 years ago

81f29f90

feat(group_theory/order_of_element): Power of subset is subgroup (#7915)

tb65536 committed 4 years ago

a83f2c26

feat(measure_theory): define `measure.trim`, restriction of a measure to a sub-sigma algebra (#7906)

RemyDegenne committed 4 years ago

ba25bb8a

feat(measure_theory/lp_space): add snorm_le_snorm_mul_rpow_measure_univ (#7926)

RemyDegenne committed 4 years ago

8377a1fc

chore(algebra/covariant_and_contravariant): fix typos in module doc-strings (#7925)

adomani committed 4 years ago

e041dbe3

feat(analysis/special_functions/trigonometric): facts about periodic trigonometric functions (#7841)

benjamindavidson committed 4 years ago

4a8ce41e

fix(tactic/induction): fix multiple cases'/induction' bugs (#7717)

JLimperg committed 4 years ago

fed7cf07

Older