leanprover-community/mathlib

Pull Requests Commits

feat(geometry/manifold/bump_function): define smooth bump functions, baby version of the Whitney embedding thm (#6839)

urkud committed 4 years ago

09110f10

JakobScholbach committed 4 years ago

fbef59ba

refactor(analysis/normed_space/basic): add semi_normed_ring (#6889)

riccardobrasca committed 4 years ago

1fdce2f8

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

leanprover-community-bot committed 4 years ago

85c89615

chore(topology/algebra/group_with_zero): continuity attributes (#6965)

hrmacbeth committed 4 years ago

8ed5c3c7

chore(data/finsupp): add simp lemmas about dom_congr (#6963)

eric-wieser committed 4 years ago

6f6ee003

refactor(data/equiv/basic): remove `equiv.set.range` (#6960)

pechersky committed 4 years ago

f2b433fa

chore(algebra/category/*): fix some names (#6846)

kim-em committed 4 years ago

cf377e2c

feat(archive/imo): add 2011 Q5 (#6927)

verberkm committed 4 years ago

33f443fc

feat(group_theory/perm/cycles): Order of is_cycle (#6873)

tb65536 committed 4 years ago

0c0fb53c

chore(algebra/direct_sum_graded): relax typeclass assumptions (#6961)

eric-wieser committed 4 years ago

a1927830

chore(group_theory/group_action/defs): combine duplicated `comp_hom` and rename derivative definitions (#6942)

eric-wieser committed 4 years ago

ed6d94a8

feat(topology/algebra/group_with_zero): continuity of exponentiation to an integer power (`fpow`) (#6937)

hrmacbeth committed 4 years ago

e1f66f1a

feat(data/set_like): remove repeated boilerplate from subobjects (#6768)

eric-wieser committed 4 years ago

bcfaabfc

chore(data/set/{basic,countable}): add, rename, golf (#6935)

urkud committed 4 years ago

b0ece6fe

feat(measure_theory/lp_space): continuous functions on compact space are in Lp (#6919)

hrmacbeth committed 4 years ago

7e109c4b

feat(analysis/normed_space/inner_product): isometry of ℂ with Euclidean space (#6877)

hrmacbeth committed 4 years ago

3e67f50c

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

Newer Older