Commits leanprover-community/mathlib3

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

feat(algebra/star/star_alg_hom): define `star_alg_equiv`s and provide basic API (#16784)

j-loreaux committed 3 years ago

69eed2f6

feat(measure_theory/measure/content): regular contents (#16289)

ReimannJ committed 3 years ago

90cde5e1

feat(data/enat/basic): more lemmas (#17143)

urkud committed 3 years ago

7ee69b10

refactor(topology/separation): redefine `t2_5_space` using `disjoint` and `nhds` (#17090)

urkud committed 3 years ago

e0d30028

feat(analysis/special_functions/complex/log): log of conjugate and inverse (#17073)

eric-wieser committed 3 years ago

8598c484

feat(data/sum/basic): add basic lemmas (#17059)

urkud committed 3 years ago

1f476e67

feat(group_theory/group_action/defs): add `smul_one_hom` (#17058)

urkud committed 3 years ago

ad104741

refactor(algebraic_geometry/*): Tidy up simp lemmas regarding `basic_open`s. (#17014)

erdOne committed 3 years ago

b599b58c

feat(data/pnat): add missing `norm_cast` attributes (#16995)

eric-wieser committed 3 years ago

0d580447

feat(group_theory/submonoid): add `*.of_mclosure_eq_top` (#16985)

urkud committed 3 years ago

4db21255

feat(algebraic_topology): variations on the statements of simplicial relations (#16957)

joelriou committed 3 years ago

5ed51dc3

feat(group_theory/coset): Add the embedding `α ⧸ (⨅ i, f i) → Π i, α ⧸ f i` (#16658)

tb65536 committed 3 years ago

a4c2bd4a

feat(category_theory/localization): basic API for localization of categories (#16969)

joelriou committed 3 years ago

1a5e56f2

feat(combinatorics/simple_graph/subgraph): single-vertex and single-edge subgraphs (#16435)

kmill committed 3 years ago

db091637

feat(data/{finset,set}/basic): A nonempty set of a subsingleton is `univ` (#16965)

YaelDillies committed 3 years ago

5b294cfe

feat(data/option/n_ary): Binary map of options (#16763)

YaelDillies committed 3 years ago

43514e1e

doc(overview,undergrad): refer to `affine_span` not `span_points` (#17130)

jsm28 committed 3 years ago

a276716e

chore: freeze data.sigma.basic (#17082)

kbuzzard committed 3 years ago

9a146627

feat(analysis/normed_space/operator_norm): characterize the operator norm over a `densely_normed_field` in terms of the supremum (#16963)

j-loreaux committed 3 years ago

b06d2285

feat(algebra/group/{ unique_prods + to_additive, counterexamples/zero_divisors_in_add_monoid_algebras.lean }): new file and to_additive dictionary (#16329)

adomani committed 3 years ago

33fa3e42

refactor(analysis/normed/group/basic): generalize `(semi)normed_group.induced` to `monoid_hom_class` and add more tools to pull back norm structures (#16255)

j-loreaux committed 3 years ago

fe67b48e

feat(group_theory/index): Add `index_eq_zero_of_relindex_eq_zero` (#16991)

tb65536 committed 3 years ago

08b57a55