Commits leanprover-community/mathlib3

Merge branch 'master' into antisymm

vihdzp committed 2 years ago

0669379d

feat (number_theory/modular_forms): holomorphy of the Jacobi theta function (#18631)

loefflerd committed 2 years ago

fe44cd36

feat(data/list/lemmas): add lemmas about `set.range list.nth*` (#18647)

urkud committed 2 years ago

2ec920d3

chore(order/category): Partially revert categories (#18690)

Parcly-Taxel committed 2 years ago

71b36b6f

chore(algebra/star/self_adjoint): generalize a lemma to `semifield` (#18687)

eric-wieser committed 2 years ago

a6ece354

feat(analysis/calculus/cont_diff): bound for the iterated derivative of a product (#18632)

sgouezel committed 2 years ago

91862a60

refactor(representation_theory/group_cohomology_resolution): refactor `k[G^{n + 1}]` isomorphism (#18271)

Amelia Livingston committed 2 years ago

c04bc6e9

fix(algebra.group.ulift): fix to_additive name for cancel_comm_monoid (#18268)

rwbarton committed 2 years ago

564bcc44

feat(set_theory/zfc/basic): define Set and Class intersection (#18232)

vihdzp committed 2 years ago

229f6f14

docs(tutorials/representation_theory): beginnings of a tutorial following Etingof's notes (#13911)

kim-em committed 2 years ago

1c775cc6

feat(data/finset/pointwise): `a • (s ∩ t) = a • s ∩ a • t` (#18682)

YaelDillies committed 2 years ago

b685f506

doc(representation_theory/basic): add docstring to dual_tensor_hom_comm (#18661)

PatrickKinnear committed 2 years ago

9cb72061

chore(linear_algebra/affine_space/combination): make k explicit in affine_combination (#18689)

mcdoll committed 2 years ago

2de9c37f

feat(ring_theory/mv_polynomial/weighted homogeneous): add weighted homogeneous polynomials (#17855)

mariainesdff committed 2 years ago

bcbee715

feat(measure_theory/group/fundamental_domain): integral_eq_tsum (#18132)

AlexKontorovich committed 2 years ago

eb810cf5

feat(category_theory/idempotents): idempotent completeness of homological_complex (#17921)

joelriou committed 2 years ago

200eda15

feat(ring_theory/ideal/norm): add ideal.finite_set_of_abs_norm_eq (#18569)

xroblot committed 2 years ago

d3acee0d

feat(set_theory/zfc/ordinal): more lemmas on transitive sets (#18307)

vihdzp committed 2 years ago

98bbc352

refactor(data/seq): scope seq and wseq to namespace stream (#18284)

arienmalec committed 2 years ago

a7e36e48

chore(scripts/list-attributes.sh): script to track attributes semireducible/irreducible (#18165)

jcommelin committed 2 years ago

95127066

feat(order/upper_lower/locally_finite): Upper closure preserves finiteness (#18678)

YaelDillies committed 2 years ago

3e175454

refactor(category_theory/shift): improve automation (#18670)

joelriou committed 2 years ago

6876fa15

chore(order/category): Rename categories (#18657)

YaelDillies committed 2 years ago

e8ac6315

feat(geometry/manifold/vector_bundle/tangent): use the new tangent bundle definition in the library (#18601)

fpvandoorn committed 2 years ago

01876449

feat(combinatorics/simple_graph/connected): support of connected components (#18442)

bottine committed 2 years ago

b99e2d58

feat(algebraic_topology/dold_kan): tools for compatibilities (#17922)

joelriou committed 2 years ago

160f568d

chore(category_theory/adjunction/opposites): backport removal of simp lemmas (#18680)

kim-em committed 2 years ago

0148d455

feat(set_theory/zfc/basic): simpler/more general `Class.ext` (#18306)

vihdzp committed 2 years ago

ef5f2ce9

chore(analysis/locally_convex/with_seminorms): remove unnecessary positivity assumption (#18659)

mcdoll committed 2 years ago

b31173ee

feat(algebra/order/monoid/min_max): `a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂` (#18667)

YaelDillies committed 2 years ago

de87d505