leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/limits/terminal): constructor for is_terminal (#6929)

kim-em committed 4 years ago

d2e59764

feat(category_theory/limits/zero): functor categories have zero morphisms (#6928)

kim-em committed 4 years ago

cf56f884

feat(algebra.smul_with_zero): add mul_zero_class.to_smul_with_zero (#6911)

eric-wieser committed 4 years ago

407ad214

feat(data/nat/basic): (n+1) / 2 ≤ n (#6863)

adomani committed 4 years ago

fe29f883

feat(category): structured arrows (#6830)

kim-em committed 4 years ago

66ee65ca

feat(category_theory): essentially_small categories (#6801)

kim-em committed 4 years ago

318cb4bc

feat(data/equiv/mul_add_aut): adding conjugation in an additive group (#6774)

ashwiniyengar committed 4 years ago

8d8b64e5

remove spurious file

sgouezel committed 4 years ago

95e9151f

sgouezel committed 4 years ago

e3a6db51

chore(group_theory/subgroup,logic/nontrivial): golf (#6934)

urkud committed 4 years ago

2ad4a4ce

sgouezel committed 4 years ago

074d3f2c

chore(topology/instances/real): remove instance `real_maps_algebra` (#6920)

hrmacbeth committed 4 years ago

5ab177a8

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

leanprover-community-bot committed 4 years ago

cb1d1c6d

feat(data/equiv/fin): rename sum_fin_sum_equiv to fin_sum_fin_equiv (#6857)

paulvanwamelen committed 4 years ago

f2900006

delete spurious file

sgouezel committed 4 years ago

2219c4a4

fix(order/complete_lattice): fix typo in docstring (#6925)

ericrbg committed 4 years ago

8e275a30

feat(measure_theory/lp_space): bounded continuous functions are in Lp (#6878)

hrmacbeth committed 4 years ago

a17f38f2

sgouezel committed 4 years ago

0526f2d7

feat(order/bounded_lattice): is_total, coe_sup and unique_maximal lemmas (#6922)

agjftucker committed 4 years ago

4487e739

feat(data/complex/circle): circle is a Lie group (#6907)

hrmacbeth committed 4 years ago

7285fb65

fix(topology/algebra/mul_action): fix typo in instance name (#6921)

eric-wieser committed 4 years ago

accb9d2d

refactor(measure_theory): add typeclasses for measurability of operations (#6832)

urkud committed 4 years ago

0e4760b3

lint(*): split long lines (#6918)

urkud committed 4 years ago

dc34b216

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

leanprover-community-bot committed 4 years ago

e129117c

feat(test/integration): add examples of computing integrals by simp (#6859)

benjamindavidson committed 4 years ago

879cb474

chore(category_theory/monads): remove empty file (#6915)

b-mehta committed 4 years ago

06b21d0f

refactor(geometry/manifold/algebra/smooth_functions): make `smooth_map_group` division defeq to `pi.has_div` (#6912)

ocfnash committed 4 years ago

27c86764

chore(topology/metric_space): golf, generalize, rename (#6849)

urkud committed 4 years ago

d1044139

refactor(representation_theory/maschke): replaces `¬(ring_char k ∣ fintype.card G)` with `invertible (fintype.card G : k)` instance (#6901)

awainverse committed 4 years ago

cc7e722a

feat(data/nat/log): add some lemmas and monotonicity (#6899)

hallow-world committed 4 years ago

d32f9c72

Newer Older