leanprover-community/mathlib3

Pull Requests Commits

chore(number_theory/well_approximable): use nat.primes (#18042)

Ruben-VandeVelde committed 3 years ago

cf73bb22

chore(*): golf (#18028)

urkud committed 3 years ago

16de0889

fix(scripts/add_port_comments): do not add PR numbers to port comments (#18030)

eric-wieser committed 3 years ago

2da281a1

chore(combinatorics/configuration): Generalize universes (#18039)

tb65536 committed 3 years ago

9830a300

chore(ring_theory/dedekind_domain/ideal): remove fractional_ideal in open namespaces (#18033)

Multramate committed 3 years ago

c3442db1

chore(*): remove references to porting PRs (#18031)

eric-wieser committed 3 years ago

448144f7

feat(ring_theory/ideal/basic): add ideal.span_pair lemmas (#18036)

Multramate committed 3 years ago

5456d487

feat(ring_theory/dedekind_domain/ideal): add fractional_ideal.coe_ideal_span_singleton mul_inv and inv_mul lemmas (#18032)

Multramate committed 3 years ago

1e05171a

refactor(data/set/finite): add `finite_to_set` lemmas to simp set (#18026)

kmill committed 3 years ago

8a8ac5bb

chore(order/closure): improve theorem statement (#18024)

ChrisHughes24 committed 3 years ago

f2528722

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

leanprover-community-bot committed 3 years ago

9aba7801

feat(number_theory/well_approximable): well-approximable numbers and Gallagher's zero-one law (#18011)

ocfnash committed 3 years ago

ffc3730d

feat(category_theory/filtered): generalize to allow empty categories (#18013)

alreadydone committed 3 years ago

14e80e85

chore(group_theory/coset): Additivise `quotient_group.preimage_mk_equiv_subgroup_times_set` (#18008)

YaelDillies committed 3 years ago

f61ffad4

chore(topology/instances/add_circle): golf (#18020)

alreadydone committed 3 years ago

a437a249

chore(group_theory/quotient_group): open `function`, use `rfl` (#18014)

urkud committed 3 years ago

09597669

fix(*): mark some classes as Prop (#18015)

urkud committed 3 years ago

986c4d57

feat(topology/instances/add_circle): expand API for finite-order points on the circle (#17986)

ocfnash committed 3 years ago

422e70f7

feat(*): bump to lean 3.50.3 (#18016)

gebner committed 3 years ago

46a64b5b

perf(analysis/inner_product_space/basic): speedups (#18018)

alreadydone committed 3 years ago

79ceafba

feat(order/locally_finite): `finset.interval` (#17939)

YaelDillies committed 3 years ago

a7b92725

feat(analysis/complex/locally_uniform_limit): compact limits of holomorphic fns are holomorphic (#17074)

vbeffara committed 3 years ago

839ab10c

feat(analysis/bounded_variation): `evariation_on` of precomposition with monotone/antitone map. (#18001)

bottine committed 3 years ago

cd9a9326

feat(analysis/complex): integration and differentiation `ℝ → ℂ` (#17989)

loefflerd committed 3 years ago

e9be2fa7

feat(algebra/geom_sum): divisibility of sums and differences of powers (#17996)

nielsvoss committed 3 years ago

8acf2263

feat(algebra/cubic_discriminant): extract useful lemma from eq_sum_three_roots (#17999)

Multramate committed 3 years ago

93013316

feat(analysis/normed_space/affine_isometry, linear_algebra/affine_space/affine_equiv): restrict affine isometry to isometry equivalence (#17522)

datokrat committed 3 years ago

09258fb7

feat(*): bump to lean 3.50.2 (#18007)

gebner committed 3 years ago

717c1321

feat(analysis/locally_convex/bounded): characterize boundedness using sequences (#17688)

ADedecker committed 3 years ago

ac1e2e08

chore(data/nat/modeq): split out lemmas about lists (#18004)

hrmacbeth committed 3 years ago

3813d4ea

Newer Older