leanprover-community/mathlib

Pull Requests Commits

Workaround: use assumption rather than apply_instance

Vierkantor committed 3 years ago

0a865275

WIP: Bump to Lean 3.36

Vierkantor committed 3 years ago

68fb59eb

urkud committed 3 years ago

6b1cba2e

doc(category_theory/limits/shapes/pullbacks): fix doc (#11225)

ericrbg committed 3 years ago

b99a98e3

feat(topology/fiber_bundle): a topological fiber bundle is a quotient map (#11194)

urkud committed 3 years ago

a30375e0

feat(algebra/opposites): add `add_opposite` (#11080)

urkud committed 3 years ago

aa82ba00

feat(data/finset/sigma): A way to lift `finset`-valued functions to a sigma type (#10958)

YaelDillies committed 3 years ago

a7aa2c87

feat(data/finset/slice): `r`-sets and slice (#10685)

YaelDillies committed 3 years ago

8bd20598

feat(analysis/inner_product_space/dual,adjoint): add some lemmas about extensionality with respect to a basis (#11176)

dupuisf committed 3 years ago

1aec9a19

feat(*): Prerequisites for the Spec gamma adjunction (#11209)

erdOne committed 3 years ago

03872fdd

chore(category_theory/limits): Generalize universes for `preserves/shapes/pullback.lean` (#10780)

erdOne committed 3 years ago

9a8e9fa5

feat(analysis/special_functions/trigonometric): a few lemmas (#11217)

urkud committed 3 years ago

044c1def

feat(algebra/order/ring): turn `mul_self_pos` into an `iff` (#11216)

urkud committed 3 years ago

3045014d

feat(linear_algebra/determinant): `det_units_smul` and `det_is_unit_smul` (#11206)

jsm28 committed 3 years ago

85784b05

chore(topology/metric_space/hausdorff_distance): slightly tidy some proofs (#11203)

Ruben-VandeVelde committed 3 years ago

1fc7a93c

feat(field_theory.intermediate_field): add intermediate_field.map_map (#11020)

Sebastian-Monnet committed 3 years ago

9d1503a6

feat(topology/maps): preimage of closure/frontier under an open map (#11189)

urkud committed 3 years ago

71dc1eab

chore(algebra/module/submodule): switch `subtype_eq_val` to `coe_subtype` (#11210)

hrmacbeth committed 3 years ago

8f391aa5

feat(data/nat/prime): factors sublist of product (#11104)

b-mehta committed 3 years ago

4daaff06

refactor(order/lexicographic): Change the `lex` synonym (#10926)

YaelDillies committed 3 years ago

62d814a4

feat(measure_theory/function/lp_space): use has_measurable_add2 instead of second_countable_topology (#11202)

RemyDegenne committed 3 years ago

9d0fd523

feat(analysis/inner_product_space/basic): negating orthonormal vectors (#11208)

jsm28 committed 3 years ago

72498958

feat(*/cyclotomic): update is_root_cyclotomic_iff to use ne_zero (#11071)

ericrbg committed 3 years ago

83f40364

feat(linear_algebra/matrix/basis): `to_matrix_units_smul` and `to_matrix_is_unit_smul` (#11191)

jsm28 committed 3 years ago

236d978d

feat(combinatorics/configuration): `has_lines` implies `has_points`, and vice versa (#11170)

tb65536 committed 3 years ago

4b3198b9

feat(algebra/big_operators/associated): `dvd_prod_iff` for `finset` and `finsupp` (#10675)

stuart-presnell committed 3 years ago

a10cb2f3

chore(algebra/algebra/spectrum): move `exists_spectrum_of_is_alg_closed_of_finite_dimensional` (#10919)

j-loreaux committed 3 years ago

a813cf5c

feat(data/polynomial/taylor): taylor_mul (#11193)

pechersky committed 3 years ago

49bf3d3e

feat(data/finset/functor): Functor structures for `finset` (#10980)

YaelDillies committed 3 years ago

a49ee49b

chore(field_theory/ratfunc): comm_ring (ratfunc K) (#11188)

pechersky committed 3 years ago

138c61fc

Older