Commits leanprover-community/mathlib3

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

feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons (#16719)

j-loreaux committed 3 years ago

63ff4532

feat(data/nat/choose/multinomial): add multinomial theorem (#16317)

pimotte committed 3 years ago

c9e2f055

feat(measure_theory/group/measure): generalise `is_haar_measure_map` slightly. (#17107)

ocfnash committed 3 years ago

62dabb94

feat(analysis/schwartz_space): Delta distribution (#16638)

mcdoll committed 3 years ago

b251b44a

feat(geometry/euclidean/oriented_angle): refactor to a basis-free definition (#16596)

hrmacbeth committed 3 years ago

f333194f

feat: add warning to scripts/port_status.py (#17132)

kim-em committed 3 years ago

ddfa266e

feat(algebraic_geometry/morphisms/universally_closed): Define universally closed morphism between schemes (#17117)

erdOne committed 3 years ago

434e2fd2

feat(ring_theory/ideal/local_ring): add lemmas about and bundled versions of `local_ring.residue_field.map` (#17104)

mkaratarakis committed 3 years ago

18b538a7