leanprover-community/mathlib

Pull Requests Commits

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

feat(linear_algebra/determinant): specialize `linear_equiv.is_unit_det` to automorphisms (#7667)

Vierkantor committed 4 years ago

f781c47e

feat(measure_theory/interval_integral): `integral_deriv_comp_mul_deriv` (#7141)

benjamindavidson committed 4 years ago

615af755

feat(algebra/char_zero): `neg_eq_self_iff` (#7916)

benjamindavidson committed 4 years ago

386962c2

docs(data/rat/denumerable): add module docstring (#7920)

YaelDillies committed 4 years ago

461b444d

feat(analysis/normed_space): nnreal.coe_nat_abs (#7911)

PatrickMassot committed 4 years ago

a853a6ae

feat(analysis/convex): add dual cone (#7738)

abentkamp committed 4 years ago

6aed9a77

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

leanprover-community-bot committed 4 years ago

fec6c8a4

feat(measure_theory/ess_sup): monotonicity of ess_sup/ess_inf w.r.t. the measure (#7917)

RemyDegenne committed 4 years ago

30045133

chore(algebra/lie/basic + classical): golf some proofs (#7903)

adomani committed 4 years ago

4fe77812

docs(set_theory/schroeder_bernstein): add module docstring (#7900)

YaelDillies committed 4 years ago

b3244884

docs(data/nat/totient): add module docstring (#7899)

YaelDillies committed 4 years ago

e971eae6

chore(measure_theory): measurability statements for coercions, coherent naming (#7854)

sgouezel committed 4 years ago

a359bd98

chore(analysis/normed_space/normed_group_hom): golf proof of normed_group_hom.bounded (#7896)

Ruben-VandeVelde committed 4 years ago

5c114586

feat(measure_theory): continuity of primitives (#7864)

PatrickMassot committed 4 years ago

2f40f351

feat(algebra/covariant_and_contravariant): API for covariant_and_contravariant (#7889)

adomani committed 4 years ago

6d2a0512

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

leanprover-community-bot committed 4 years ago

7c9643de

docs(data/nat/pairing): add module docstring (#7897)

YaelDillies committed 4 years ago

e13fd486

chore(algebra/{ordered_group, linear_ordered_comm_group_with_zero.lean}): rename one lemma, remove more @s (#7895)

adomani committed 4 years ago

2c919b08

feat(group_theory/group_action/defs): add `has_mul.to_has_scalar` and relax typeclass in `smul_mul_smul` (#7885)

ocfnash committed 4 years ago

add577d7

chore(category_theory/filtered): Adds missing instances (#7909)

adamtopaz committed 4 years ago

e0a3303f

Newer Older