Commits leanprover-community/mathlib

feat(topology/algebra/group): quotient of a second countable group (#16738)

AlexKontorovich committed 3 years ago

ce4a8b89

refactor(data/set/basic): review API of `set.nontrivial` (#16737)

urkud committed 3 years ago

7802ba77

feat(geometry/euclidean/basic): angles and betweenness (#16734)

jsm28 committed 3 years ago

6d5dda18

feat(tactic/positivity): Extensions for `nat` constructions (#16728)

YaelDillies committed 3 years ago

b0b0d5e3

feat(logic/relation): characterization of the accessible predicate in terms of `well_founded_on` (#16720)

alreadydone committed 3 years ago

5ca6e9d2

feat(ring_theory/graded_algebra/homogeneous_localization): generalise homogeneous localization to any submonoid (#16653)

jjaassoonn committed 3 years ago

486cb2f3

feat(topology/algebra/continuous_monoid_hom): Continuity of composition (#16319)

tb65536 committed 3 years ago

5cf34f8f

chore(data/seq/*): `cases_on` → `rec_on` (#15843)

vihdzp committed 3 years ago

77615d00

feat(ring_theory/dedekind_domain/selmer_group): add Selmer groups of Dedekind domains (#15405)

Multramate committed 3 years ago

9aec1a28

feat(set_theory/game/birthday): birthday of addition equals natural addition of birthdays (#14549)

vihdzp committed 3 years ago

a3470769

feat(set_theory/surreal/basic): relabellings preserve being numeric (#14406)

vihdzp committed 3 years ago

ee02a30e

feat(linear_algebra/affine_space/affine_subspace): spans of two points (#16770)

jsm28 committed 3 years ago

eb973896

feat(analysis/convex/between): `wbtw` and distinct end points (#16768)

jsm28 committed 3 years ago

f1f9d66a

feat(analysis/convex/between): betweenness and `same_ray` (#16767)

jsm28 committed 3 years ago

580e52cb

feat(linear_algebra/affine_space/affine_subspace): `vector_span_insert_eq_vector_span` (#16765)

jsm28 committed 3 years ago

64b6d04f

refactor(number_theory): reorganize number field results into new subfolder (#16764)

xroblot committed 3 years ago

81120aec

feat(data/{fin,}set/pointwise): add `{fin,}set.inv_insert` (#16748)

urkud committed 3 years ago

8a1b982f

refactor(data/fin/basic): merge `fin.rev` and `order_iso.fin_equiv` (#16745)

urkud committed 3 years ago

c7aa2dfa

fix({ tactic/fin_cases + test/interval_cases }): add `focus1` and a test (#16752)

adomani committed 3 years ago

9dbe038e

feat(category_theory/groupoid/free): free groupoid on a quiver (#16666)

bottine committed 3 years ago

2e433a50

feat(group_theory/subgroup): add several trivial lemmas (#16633)

urkud committed 3 years ago

35bc69bc

feat(data/fintype/basic): Existence of a bijection with specified behaviour on a subset (#16479)

hrmacbeth committed 3 years ago

3cf2547c

chore(analysis/locally_convex/with_seminorms): fix namespaces for dot-notation (#16771)

mcdoll committed 3 years ago

d2461773

feat(analysis/normed/group/add_circle): define the additive circle (#16201)

ocfnash committed 3 years ago

ebe6bda5

feat(algebra/module/projective): weaken assumptions in lifting_property (#16750)

antoinelab01 committed 3 years ago

08bb56fb

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

leanprover-community-bot committed 3 years ago

8818d823

feat(analysis/convex/cone/basic): add `has_add`, `add_zero_class`, and `add_comm_semigroup` instances to `convex_cone` (#16213)

apurvnakade committed 3 years ago

3665254a

feat(linear_algebra/matrix/hermitian): complex_hermitian_real_diagonal (#16380)

mapehe committed 3 years ago

a4e0a656

feat(order/liminf_limsup): add limsup/liminf variants of some Limsup/Liminf lemmas (#16759)

RemyDegenne committed 3 years ago

b2d70ba0

docs(analysis/locally_convex/bounded): fix hyperlink (#16753)

mcdoll committed 3 years ago

2ce380c2