leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 2 years ago

1e25812b

eric-wieser committed 2 years ago

9f725bb8

Merge remote-tracking branch 'origin/master' into eric-wieser/simplify-language

eric-wieser committed 2 years ago

b1397096

chore(data/set/semiring): add an `idem_semiring` instance (#18449)

eric-wieser committed 2 years ago

a51ce549

feat(set_theory/zfc/basic): induction principle for sets (#18324)

vihdzp committed 2 years ago

d7feae34

feat(order/game_add): `sym2.game_add` (#18287)

vihdzp committed 2 years ago

7b1d4abc

chore(geometry/manifold/vector_bundle): golf (#18509)

urkud committed 2 years ago

87ecf961

refactor(topology/*): add `uniform_space.of_fun`, use it (#18495)

urkud committed 2 years ago

e1a7bdeb

fix(geometry/manifold/vector_bundle): fix timeout (#18507)

fpvandoorn committed 2 years ago

23a3e7d9

feat(data/list/basic): missing lemmas about `list.enum` (#18489)

eric-wieser committed 2 years ago

9da1b353

refactor(number_theory/pell): Small golf using `int.eq_of_mul_eq_one` (#18505)

tb65536 committed 2 years ago

35c1956c

feat(algebra/order/ring/canonical): add `canonically_ordered_comm_semiring.to_ordered_comm_monoid` (#18504)

urkud committed 2 years ago

824f9ae9

fix(data/finmap): `finmap.all` should not always be `ff` (#18432)

eric-wieser committed 2 years ago

c3fc15b2

feat(geometry/euclidean/angle/unoriented): sine & cosine angle lemmas (#18222)

JovanGerb committed 2 years ago

aedfb56f

feat(linear_algebra/bilinear_form/tensor_product): tensor product of bilinear forms (#18211)

eric-wieser committed 2 years ago

f91d3736

feat(data/nat/multiplicity): rename `nat.multiplicity_choose_prime_pow`, add lemmas (#18183)

urkud committed 2 years ago

114ff8a4

chore(data/real/ennreal): drop some lemmas (#18501)

urkud committed 2 years ago

57ac39bd

feat(algebraic_geometry/elliptic_curve/point): define homomorphism induced by base change (#18493)

Multramate committed 2 years ago

03994e05

feat(data/int/units): If `z * w = 1`, then `z = w` (#18499)

tb65536 committed 2 years ago

45a1ada0

docs(algebra/module/equiv): correct a misleading comment (#18458)

eric-wieser committed 2 years ago

ea94d7cd

refactor(topology/metric_space): drop `dist_setoid` (#18502)

urkud committed 2 years ago

0c1f285a

feat(matrix/dual_number): `matrix` and `dual_number` commute (#18386)

eric-wieser committed 2 years ago

eb0cb451

chore(number_theory/pell*): rename files, update doc (#18503)

MichaelStollBayreuth committed 2 years ago

a66d07e2

feat(set_theory/ordinal/fixed_point): add missing theorem (#18323)

vihdzp committed 2 years ago

c6b53304

fix (measure_theory/measure/measure_space_def): fix module docstring typos (#18500)

kbuzzard committed 2 years ago

146a2eed

docs(set_theory/lists): update docs (#18346)

astrainfinita committed 2 years ago

497d1e06

chore(data/finset/lattice): Protect a few more lemmas (#18497)

YaelDillies committed 2 years ago

1c857a1f

feat(data/polynomial/div): prove that evaluation induces an isomorphism of algebras (#18480)

Multramate committed 2 years ago

e064a7bf

feat(number_theory/pell_general): add general existence result for Pell's Equation (#18484)

MichaelStollBayreuth committed 2 years ago

c23aca35

feat(analysis/fourier): Poisson summation (#18392)

loefflerd committed 2 years ago

3353f337

Older