Changelog
2023-11-29 00:23 b9d519bb
refactor(*/Multilinear): change `*.ofSubsingleton` (#8694) …
7 files10 theorems6 defs
2023-11-28 21:58 0cac4cb3
feat: Add `Polynomial.separable_map'`. (#8680)
1 files1 theorems
2023-11-28 20:47 df0fd9f3
feat: composition of a multilinear map and linear maps is multilinear (#8687)
1 files
2023-11-28 20:10 ad70e022
feat: multilinearity of the `MultilinearMap.compLinearMap` operation (#8684)
1 files2 defs
2023-11-28 18:48 ce7d2c1b
feat(Topology/GDelta): rename "nowhereDense" to "isNowhereDense" (#8567) …
1 files6 theorems
2023-11-28 18:28 d6652f77
fix: CI badge appears twice in readme (#8689)
1 files
2023-11-28 18:08 c28500a0
feat(CategoryTheory/Sites): internal hom of (pre)sheaves (#8622) …
6 files7 theorems2 defs
2023-11-28 15:55 60b5e237
feat(FieldTheory/SeparableDegree): basic definition of separable degree of field extension (#8117) …
3 files34 theorems15 defs
2023-11-28 14:52 547a8415
refactor: use the new homology API for right derived functors (#8593) …
8 files47 theorems16 defs
2023-11-28 14:52 2bfea869
feat(CategoryTheory): the localized category of a product category (#8516) …
5 files14 theorems3 defs
2023-11-28 14:52 b4ed5810
feat(CategoryTheory): naturality of the connecting homomorphism of the snake lemma (#8490) …
1 files11 theorems6 defs1 structures
2023-11-28 14:12 4bfed3e4
feat: weights of Lie modules are linear functions (#8677) …
4 files6 theorems1 defs
2023-11-28 12:41 88b4f4c7
feat: Relax arguments of going-up theorems. (#8645)
1 files7 theorems
2023-11-28 11:57 baf37635
feat: `IsFractionRing R R` if `R` is a field. (#8641)
3 files2 theorems
2023-11-28 11:15 65fce9bb
feat: Add lemmas about `Polynomial.scaleRoots`. (#8653)
2 files16 theorems
2023-11-28 09:41 39b23fff
feat: Add `IsAlgebraic.inv_iff`. (#8651)
1 files3 theorems
2023-11-28 08:56 666326ce
feat: add some results about IsCyclic (#8625) …
1 files3 theorems
2023-11-28 08:01 3f88a472
refactor(Probability/Density): define pdf using rnDeriv (#8544) …
5 files50 theorems1 defs
2023-11-28 07:37 d835056c
feat: computation of the connecting homomorphism of the snake lemma in concrete categories (#8512) …
3 files3 theorems
2023-11-28 06:13 dc2eb24d
chore: bump dependencies (#8671)
1 files
2023-11-28 04:40 16f64a1d
chore: build lean4checker with current toolchain (#8669) …
4 files
2023-11-28 03:17 2577ef78
chore: bump for std4#241 (#6975) …
16 files3 defs
2023-11-28 01:23 aa204e9a
Update docstring of `squeeze_one_norm'` (#8667) …
1 files
2023-11-28 00:02 7cc262f3
fix(Cache): correctly handle local copies of `Mathlib` (#8662) …
3 files3 defs
2023-11-27 21:37 3c30dbb2
feat: a family of generalized eigenvalues for a commuting linear family of endomorphims must be linear (#8656)
1 files4 theorems
2023-11-27 20:16 c77ae20f
feat: bounds for Dirichlet characters (#8449) …
4 files3 theorems
2023-11-27 18:31 313ebb43
feat: Add `AlgHom.map_adjoin_singleton`. (#8655)
1 files1 theorems
2023-11-27 17:05 fa1d892a
feat: Add `Submodule.restrictScalars_mul`. (#8649)
1 files1 theorems
2023-11-27 17:05 27d3a24e
feat: Add `not_isNilpotent_one`. (#8648)
1 files1 theorems
2023-11-27 17:05 098e254c
feat(Data/Set/Lattice): generalize `Set.iUnion_univ_pi` (#8647) …
1 files1 theorems
2023-11-27 17:05 04c2181e
feat(Topology/Bornology): add convenience lemmas (#8640) …
1 files3 theorems
2023-11-27 16:21 187f84fb
feat: remove an assumption (#8646) …
1 files1 theorems
2023-11-27 15:05 b70e89f1
feat(SpecialFunctions/Log): add `tendsto_log_nhdsWithin_zero_right` (#8554) …
1 files1 theorems
2023-11-27 14:14 1412ef2f
feat(LinearAlgebra/TensorProduct): add `liftAddHom` (#8584) …
1 files1 theorems1 defs
2023-11-27 11:28 c1f4e113
chore: update the nightly-with-mathlib branch at leanprover/lean4 (#8628) …
1 files
2023-11-27 11:06 efd29612
chore: merge master into nightly-testing via cron, not on every commit (#8627) …
1 files
2023-11-27 11:06 319c50be
chore: `ValuedCsp` and `ValuedCsp.Instance` changed from `def` to `abbrev` (#8623)
1 files2 defs
2023-11-27 10:05 3f5910bf
feat(Data/Finset/Card): add converse to some existing theorems (#8515) …
2 files5 theorems
2023-11-27 10:05 4b30f25b
refactor(Data/Matrix/Basic): use a defeq for scalar that matches its docstring (#8115) …
8 files14 theorems
2023-11-27 09:11 55eb8124
chore(GroupTheory/Congruence): small cleanups (#8314) …
2 files9 theorems
2023-11-26 22:11 83d4f222
chore: add docs + alias for `prod_bijective` (#8439)
1 files
2023-11-26 21:03 4e2498ef
chore: implement simp_rw config matching better (#8592)
1 files
2023-11-26 13:22 12d7898d
chore: bump dependencies (#8626)
1 files
2023-11-26 04:56 c159834a
fix: patch for std4#203 (more sub lemmas for `Nat`) (#6216)
21 files2 theorems
2023-11-25 18:19 632ea778
chore: delete `LinearMap.extendScalars` which duplicates `LinearMap.baseChange` (#8617) …
6 files31 theorems5 defs
2023-11-25 17:55 4b97b736
doc(Computability/Halting): Mark named theorems (#8577) …
4 files
2023-11-25 17:07 a538c320
feat: prove an upper bound on bitwise operations (#8598) …
1 files4 theorems
2023-11-25 15:38 706be658
doc: add a better docstring for `fun₀` (#8601)
1 files
2023-11-25 15:15 1c6e8b59
chore: Fix universe (misprint in Portmanteau.lean). (#8620) …
1 files
2023-11-25 10:19 5ddf761e
feat(AlgebraicGeometry): the big Zariski site (#8549) …
3 files2 theorems2 defs