leanprover-community/mathlib3

Pull Requests Commits

kim-em committed 3 years ago

b2748e31

kim-em committed 3 years ago

6f8d1eeb

change back to trace

kim-em committed 3 years ago

acf60055

kim-em committed 3 years ago

f63477d5

kim-em committed 3 years ago

15595eca

kim-em committed 3 years ago

f45dc244

feat(tactic/abel): separate out abel_nf

kim-em committed 3 years ago

a5d845a9

feat(data/set/intervals/basic): Injectivity of half-infinite intervals (#17157)

mans0954 committed 3 years ago

438381a5

chore(data/set/pointwise): split file, reducing dependencies (#16950)

kim-em committed 3 years ago

aa329229

feat(algebra/order/floor): some nat.ceil lemmas (#16987)

alexjbest committed 3 years ago

ad7dca6a

docs(src/order/locally_finite.lean): fix a copy-paste typo (#17196)

adomani committed 3 years ago

192f43c6

feat(analysis/normed_space/star/gelfand_duality): realize the Gelfand transform as a `star_alg_equiv` (#17167)

j-loreaux committed 3 years ago

30415257

feat(algebra/group_power/order): add `pow_lt_self_of_lt_one` (#17162)

urkud committed 3 years ago

5118ae32

feat(data/fintype/basic): lemmas about `finset.univ` (#17067)

urkud committed 3 years ago

5155be47

chore(algebra/group/to_additive): move to tactic/ (#17182)

kim-em committed 3 years ago

8308d266

chore(counterexamples/zero_divisors_in_add_monoid_algebras): sort imports (#17152)

adomani committed 3 years ago

ad47ef8a

feat(topology/algebra/const_mul_action): `order_dual` instances (#17125)

YaelDillies committed 3 years ago

94a228cf

feat(topology/continuous_function/algebra): precomposition with a homeomorphism as a `star_alg_equiv` (#17166)

j-loreaux committed 3 years ago

6d37f402

fix(algebraic_geometry/morphisms/universally_closed): Fix docstring. (#17135)

erdOne committed 3 years ago

a8ae1b3f

refactor(group_theory/order_of_element): Remove `fintype` hypothesis from `pow_coprime` (#16989)

tb65536 committed 3 years ago

179dcdea

chore(analysis/inner_product_space/basic): remove `bilin_form_of_real_inner` (#15780)

mcdoll committed 3 years ago

ec3c1f27

feat(algebra/free_monoid): add `decidable_eq` instance (#17163)

urkud committed 3 years ago

43efa804

chore(measure_theory/measure/giry_monad): add spaces, golf (#17155)

RemyDegenne committed 3 years ago

c7d6e642

feat(data/bool/basic): add several lemmas (#17153)

urkud committed 3 years ago

44c394bb

chore(order/cover): add `covby.eq_of_between` (#17146)

eric-wieser committed 3 years ago

3b3cd894

feat(analysis/special_functions/trigonometric/inverse): `tan_arcsin`, `tan_arccos`, `arccos_eq_arcsin`, `arcsin_eq_arccos` (#17105)

jsm28 committed 3 years ago

cc26a6cb

feat(data/set/pairwise): Taking the `bUnion` is injective (#17052)

YaelDillies committed 3 years ago

23ffd4ac

feat(algebra/module/submodule/basic): add `submodule_class` and `smul_mem_class` (#16134)

j-loreaux committed 3 years ago

12a7da10

feat(topology/instances/discrete): the discrete topology is metrizable (#17145)

RemyDegenne committed 3 years ago

71a9381e

feat(probability/independence): lemmas about pi_Union_Inter of a sequence of singletons (#17013)

RemyDegenne committed 3 years ago

cc365b5c

Older