Commits leanprover-community/mathlib3

feat(group_theory/subgroup/basic): The center can be written as the intersection of centralizers (#16837)

tb65536 committed 3 years ago

45ef183d

feat(topology/instances/add_circle): the additive circle `ℝ / (a ∙ ℤ)` is normal (T4) and second-countable (#16594)

hrmacbeth committed 3 years ago

0fbd703b

feat(topology/separation): add instances about `separation_quotient` (#16579)

urkud committed 3 years ago

43e95eef

feat(measure_theory/integral/riesz_markov_kakutani): begin construction of content for Riesz-Markov-Kakutani (#16367)

ReimannJ committed 3 years ago

7bbc52b7

feat(geometry/euclidean/oriented_angle): oriented angles and betweenness (#16824)

jsm28 committed 3 years ago

34c70db6

feat(geometry/euclidean/oriented_angle): collinearity and affine independence (#16822)

jsm28 committed 3 years ago

abed0373

feat(linear_algebra/affine_space/independent): affine independence of all but one point (#16815)

jsm28 committed 3 years ago

069c3d1e

feat(group_theory/submonoid/basic): add `monoid_hom.of_mclosure_eq_top_left` (#16809)

urkud committed 3 years ago

c8243a6a

feat(linear_algebra/affine_space/finite_dimensional): more `collinear` lemmas (#16806)

jsm28 committed 3 years ago

419c83f6

chore(tactic/linarith): remove unneeded code (#16791)

kim-em committed 3 years ago

3348bed9

feat(analysis/analytic/uniqueness): two analytic functions that coincide locally coincide globally (#16723)

sgouezel committed 3 years ago

476f28f8

feat(analysis/calculus): bounded variation functions (#16683)

sgouezel committed 3 years ago

aadde303

feat(algebra/algebra/basic): make algebra_map a low prio has_lift_t (#16567)

kbuzzard committed 3 years ago

d840349d

feat(ring_theory/valuation): Equivalent conditions of DVRs. (#15081)

erdOne committed 3 years ago

10a3d03b

refactor(analysis/normed_space/spectrum): remove `norm_one_class` hypotheses (#16891)

j-loreaux committed 3 years ago

71a08c30

chore(ring_theory.dedekind_domain.adic_valuation): delete outdated comment (#16886)

mariainesdff committed 3 years ago

d20f598e

feat(topology/algebra/group): discrete subgroup acts properly discontinuously (#16593)

hrmacbeth committed 3 years ago

c476f200

fix(.github/CODEOWNERS): disable catch-all pattern for now (#16892)

jcommelin committed 3 years ago

fbfef5a1

feat(measure_theory/measure/haar_lebesgue): the Lebesgue measure is doubling (#16885)

sgouezel committed 3 years ago

09b58946

doc(order/filter/zero_and_bounded_at_filter): tinker with docstrings (#16874)

kbuzzard committed 3 years ago

07a2c0d8

chore(.github): add CODEOWNERS stub (#16846)

jcommelin committed 3 years ago

874b4ab7

feat(topology/basic): Singleton sets are not open (#16843)

tb65536 committed 3 years ago

4f569375

feat(topology/metric_space/basic): `positivity` extension for `diam` (#16842)

YaelDillies committed 3 years ago

3441411d

feat(data/list/basic): Alias for `length_le_of_sublist` (#16841)

YaelDillies committed 3 years ago

11156f5a

chore(data/int/gcd): streamline imports (#16811)

hrmacbeth committed 3 years ago

103252ae

feat(ring_theory/integral_closure): Generalize `is_integral_algebra_map_iff` to noncommutative setting. (#16880)

erdOne committed 3 years ago

b381419c

chore(order/lattice): remove redundant imports (#16877)

kim-em committed 3 years ago

2af511a7

chore(topology/continuous_function/algebra): fix an unexplained issue with `continuous_map.coe_fn_alg_hom` (#16876)

j-loreaux committed 3 years ago

ad6bbaf4

perf(topology/sheaves/presheaf_of_functions): speedups (#16873)

alreadydone committed 3 years ago

6c31dd65

chore(analysis/normed_space/star/complex): delete file (#16871)

j-loreaux committed 3 years ago

8434f767