leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into height_one_spectrum

Multramate committed 3 years ago

af7bd5d8

chore(number_theory/number_field/basic): fix a name (#16943)

riccardobrasca committed 3 years ago

29761083

feat(ring_theory/dedekind_domain/ideal): height_one_spectrum is equivalent to maximal_spectrum (#16920)

Multramate committed 3 years ago

5147123e

feat(algebra/group_with_zero/units): add ring.inverse lemmas (#16889)

mariainesdff committed 3 years ago

9644d968

chore(algebra/order/sub): split file (#16868)

kim-em committed 3 years ago

02b85de4

chore(tactic/core): fix bug in `resolve_attribute_expr_list` (#16827)

hrmacbeth committed 3 years ago

938f1f1b

feat(order/liminf_limsup): define `filter.blimsup`, `filter.bliminf` (#16819)

ocfnash committed 3 years ago

856cfd48

feat(topology/sheaves): Localization of a sheaf. (#15331)

erdOne committed 3 years ago

8b80cafb

feat(data/set/fintype): Add `to_finset_nonempty`. (#16925)

linesthatinterlace committed 3 years ago

080cbe2f

feat(data/set/finite): Add `off_diag` finitary instance and lemmas (#16923)

linesthatinterlace committed 3 years ago

1a170053

feat(data/int/gcd): add lemmas on gcd with negatives (#16922)

alainchmt committed 3 years ago

1675aa42

feat(linear_algebra/matrix): inverse of block triangular is block triangular (#16150)

YaelDillies committed 3 years ago

46fc73a3

refactor(geometry/euclidean): split up unoriented angles (#16942)

jsm28 committed 3 years ago

f8b900bf

chore(group_theory/*): Golf using `subgroup.subtype_injective` (#16941)

tb65536 committed 3 years ago

f2259302

feat(geometry/euclidean/basic): `concyclic` (#16927)

jsm28 committed 3 years ago

8f82d25e

refactor(algebra/free_monoid): add `to_list`/`of_list` (#16926)

urkud committed 3 years ago

fc2e3b00

feat(group_theory/perm): add `equiv.perm.equiv_units_End` (#16900)

urkud committed 3 years ago

74cf64c3

feat(analysis/convex/between,analysis/convex/side): betweenness and `point_reflection` (#16937)

jsm28 committed 3 years ago

8b7c3f5b

feat(measure_theory/covering/differentiation): Lebesgue differentiation theorem (#16906)

sgouezel committed 3 years ago

f45d3379

feat(data/finset/prod): image projections out of finset product (#16936)

b-mehta committed 3 years ago

4dc9ec77

feat(analysis/calculus/monotone): a monotone function is differentiable almost everywhere (#16549)

sgouezel committed 3 years ago

c9f6b6f0

Merge remote-tracking branch 'origin/master' into height_one_spectrum

Multramate committed 3 years ago

0700950d

feat(number_theory/number_field): add map_mem_ring_of_integers (#16754)

riccardobrasca committed 3 years ago

65fbcb33

feat(analysis/convex/side): betweenness and affine subspaces (#16733)

jsm28 committed 3 years ago

357b2966

chore(.github/CODEOWNERS): two new rules (#16921)

jcommelin committed 3 years ago

b49d5686

feat(group_theory/transfer): The kernel of the transfer homomorphism `G →* P` is disjoint from every `p`-group (#16914)

tb65536 committed 3 years ago

6979111c

refactor(set_theory/cardinal): review API about `#α = 2`/`nat.card α = 2` (#16899)

urkud committed 3 years ago

73ccd02e

feat(combinatorics/quiver/path): Composition is injective (#16852)

YaelDillies committed 3 years ago

98c944e9

feat(topology/algebra/infinite_sum): infinite sums on subsets (#16671)

fpvandoorn committed 3 years ago

6ef05bb3

feat(topology/basic): add `is_closed.interior_union` and `is_closed.interior_union'` (#16599)

astrainfinita committed 3 years ago

5ef85df4

Older