leanprover-community/mathlib

Pull Requests Commits

kim-em committed 4 years ago

032f77b8

chore(algebra/big_operators/order): generalize some lemmas to `ordered_comm_semiring` (#6950)

urkud committed 4 years ago

877af106

feat(topology/compact_open): β ≃ₜ C(α, β) if α has a single element (#6946)

TwoFX committed 4 years ago

fe00980a

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

leanprover-community-bot committed 4 years ago

8d398a8f

feat(group_theory/order_of_element): exists_pow_eq_self_of_coprime (#6875)

tb65536 committed 4 years ago

b4ce9b7f

feat(order/ideal, order/pfilter, order/prime_ideal): added `is_ideal`, `is_pfilter`, `is_prime`, `is_maximal`, `prime_pair` (#6656)

atarnoam committed 4 years ago

b449a3cd

feat(category_theory/arrow): simp lemmas for lifts involving arrow.mk (#6953)

TwoFX committed 4 years ago

e5c112d6

feat(group_theory/{subgroup, order_of_element}): refactors simple groups, classifies finite simple abelian/solvable groups (#6926)

awainverse committed 4 years ago

87bc893a

feat(topology/local_homeomorph): add `is_image`, `piecewise`, and `disjoint_union` (#6804)

urkud committed 4 years ago

ad4aca0c

feat(data/fin): fin n.succ is an add_comm_group (#6898)

eric-wieser committed 4 years ago

50225dad

chore(topology/instances/real): golf (#6945)

urkud committed 4 years ago

8b7c8a4c

chore(topology/instances/ennreal): golf (#6944)

urkud committed 4 years ago

3fdf5295

chore(*): long lines (#6939)

kim-em committed 4 years ago

16776539

feat(category_theory/images): instance for precomposition by iso (#6931)

kim-em committed 4 years ago

f1fe129e

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

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

urkud committed 4 years ago

2ad4a4ce

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

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

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

Older