leanprover-community/mathlib

Pull Requests Commits

Don't need this type ascription anymore

Vierkantor committed 4 years ago

58bbbae0

`simp` can't already prove this, because we're no longer going through `coe_fn_trans`

Vierkantor committed 4 years ago

b9b8fdfa

Use more `ring_hom_class` lemmata for `alg_hom`

Vierkantor committed 4 years ago

28e339f7

Merge remote-tracking branch 'mathlib/master' into Vierkantor/polynomial-spectral-mapping

Vierkantor committed 4 years ago

89a8a0cc

Use generic `commutes.map` lemma

Vierkantor committed 4 years ago

fd28f5f5

feat(algebra/group/hom): generalize `semiconj_by.map` and `commute.map`

Vierkantor committed 4 years ago

965d9e5b

feat(algebra/algebra): instantiate `ring_hom_class` for `alg_hom`

Vierkantor committed 4 years ago

1c21dc1a

feat(topology/subset_properties): open/closed sets are locally compact spaces (#10844)

urkud committed 4 years ago

5558fd9f

feat(combinatorics/simple_graph/basic): Incidence set lemmas (#10839)

YaelDillies committed 4 years ago

b100af69

refactor(category_theory/sites/*): Redefine the category of sheaves. (#10678)

adamtopaz committed 4 years ago

9f9015c6

fix(ring_theory/ideal/basic): remove universe restriction (#10843)

eric-wieser committed 4 years ago

601f2ab7

chore(field_theory/ratfunc): to_fraction_ring_ring_equiv (#10806)

eric-wieser committed 4 years ago

905d887f

chore(field_theory/ratfunc): has_scalar in terms of localization (#10828)

pechersky committed 4 years ago

eeef771d

feat(data/set/function): Congruence lemmas for `monotone_on` and friends (#10817)

YaelDillies committed 4 years ago

542471fd

feat(ring_theory/local_property): Being reduced is a local property. (#10734)

erdOne committed 4 years ago

b5b19a69

chore(analysis/mean_inequalities_pow): nnreal versions of some ennreal inequalities (#10836)

hrmacbeth committed 4 years ago

68ced9a9

feat(measure_theory/measure): new class is_finite_measure_on_compacts (#10827)

sgouezel committed 4 years ago

d212f3eb

feat(category_theory/adjunction/evaluation): Evaluation has a left and a right adjoint. (#10793)

adamtopaz committed 4 years ago

87e2f24b

update documentation after renaming

j-loreaux committed 4 years ago

Verified 08b27d94

chore(data/polynomial/field_division): beta-reduce (#10835)

gebner committed 4 years ago

8e4b3b0f

chore(*): tweaks taken from gh-8889 (#10829)

eric-wieser committed 4 years ago

5a835b7b

feat(analysis/normed_space/basic): formula for `c • sphere x r` (#10814)

urkud committed 4 years ago

8218a788

feat(topology/metric_space/isometry): (pre)image of a (closed) ball or a sphere (#10813)

urkud committed 4 years ago

b82c0d25

feat(topology/metric_space/hausdorff_distance): add more topological properties API to thickenings (#10661)

kkytola committed 4 years ago

21c9d3b3

change names and switch order of rewriting

j-loreaux committed 4 years ago

Verified 321458b3

include small `list_prod_is_unit` lemma in proof of main theorem

j-loreaux committed 4 years ago

Verified 96de1ff9

chore(topology/continuous_function/bounded): remove extra typeclass assumption (#10823)

hrmacbeth committed 4 years ago

ef69cac1

feat(algebra/module/linear_map): interaction of linear maps and pointwise operations on sets (#10821)

sgouezel committed 4 years ago

00c55f5e

feat(analysis/special_functions/complex): range of `complex.exp (↑x * I)` (#10816)

urkud committed 4 years ago

dfb78f7e

feat(analysis/mean_inequalities): corollary of Hölder inequality (#10789)

hrmacbeth committed 4 years ago

81e58c9e

Older