Commits leanprover-community/mathlib

Update src/algebra/category/Group/injective.lean

jjaassoonn committed 2 years ago

Verified b5023caa

Update src/group_theory/order_of_element.lean

jjaassoonn committed 2 years ago

Verified a11edfb2

fix linter

jjaassoonn committed 3 years ago

3b3724e4

Merge remote-tracking branch 'origin/master' into jjaassoonn/div_res_infinite

jjaassoonn committed 3 years ago

36bb336e

Merge branch 'jjaassoonn/div_res_infinite' of https://github.com/leanprover-community/mathlib into jjaassoonn/div_res_infinite

jjaassoonn committed 3 years ago

48d7f0f8

perf(algebra/category/Module/monoidal): fix timeout (#16903)

alreadydone committed 3 years ago

556f3534

feat(category_theory): categories where inclusions into coproducts are mono (#16867)

joelriou committed 3 years ago

23d1b33c

chore(algebra/ring/basic): move results on dvd (#16864)

kim-em committed 3 years ago

b1aef433

feat(group_theory/subgroup/pointwise): Basic lemmas (#16856)

tb65536 committed 3 years ago

21926ffe

feat(ring_theory/etale): Formally unramified iff `Ω[S⁄R] = 0` (#16849)

erdOne committed 3 years ago

03eaefc4

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

Merge branch 'master' into jjaassoonn/div_res_infinite

jcommelin committed 3 years ago

f15586d7

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