Changelog

2024-02-29 21:30 a424c094
feat: `IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M` (#10918) …
4 files6 theorems
2024-02-29 18:56 77166edf
feat: Add norm_iteratedFDeriv_prod_le using Sym (#10022) …
9 files45 theorems
2024-02-29 18:30 a9842983
feat: filtered category is finally small if there is a small weakly terminal set (#10949)
1 files6 theorems
2024-02-29 17:22 64848f61
add two to_additive name translations (#10831) …
11 files5 theorems
2024-02-29 15:38 3eced184
fix(Data/Finset): don't show a warning if `proveFinsetNonempty` fails (#11072) …
2 files
2024-02-29 14:27 45041bba
feat: Equivalent characterizations of lower- and upper-semicontinuous functions (#7851) …
1 files10 theorems
2024-02-29 13:07 0aaf3be3
doc(LinearAlgebra/PiTensorProduct): improve docstring for tprod notation (#11063) …
1 files
2024-02-29 12:38 2353c4e3
fix(LinearAlgebra/TensorPower): correct notation precedence (#11062) …
2 files10 theorems6 defs
2024-02-29 12:38 73d45f44
split power series in several files (#10866) …
11 files322 theorems32 defs
2024-02-29 12:10 d1e0bc52
chore: classify `broken proof was` porting notes (#11040) …
3 files
2024-02-29 11:10 a4e76ac4
refactor(LinearAlgebra/ExteriorAlgebra/{Basic,Grading}): add a definition and notation for the exterior powers of a module (#10744) …
2 files1 theorems
2024-02-29 10:41 925c6abe
feat: `positivity` extensions for `Finset.card`, `Fintype.card` (#10610) …
4 files2 defs
2024-02-29 09:37 2f2096e5
chore(Data/Finset/Lattice): better docs for `gcongr` lemmas (#11067) …
2 files
2024-02-29 09:37 51b9fc49
chore: Generalise big operators lemmas to `PosMulMono` (#10875) …
1 files1 theorems
2024-02-29 08:53 10672055
chore(Topology/Algebra/InfiniteSum): split up large file (#11050) …
10 files270 theorems4 defs
2024-02-29 02:46 7ca43cbd
chore: bump toolchain to v4.6.0 (#11065)
8 files
2024-02-29 02:01 13e13156
feat(CategoryTheory/Monoidal): redefine `tensorLeft` by using whiskering (#10898) …
8 files25 theorems
2024-02-29 00:55 efdfa67f
feat(Finset): add `gcongr` attributes (#9520)
4 files3 theorems
2024-02-28 23:16 d8924e0a
feat(LinearAlgebra/Matrix/Adjugate): adjugate_fin_three, adjugate_fin_three_of (#11005) …
1 files2 theorems
2024-02-28 22:21 eaf18cb1
feat : rework enough-injectiveness proof of groups using character module (#8559) …
5 files10 theorems3 defs
2024-02-28 21:39 aa178a85
refactor(LinearAlgebra/Matrix/Adjugate): shorten proof of adjugate_fin_two (#11051)
1 files
2024-02-28 20:02 dce76308
feat(CategoryTheory): the recognition theorem for ind-objects (#10973)
1 files4 theorems
2024-02-28 17:59 449a4a9b
feat: `ℕ`, `ℤ` and `ℚ≥0` are star-ordered rings (#10633) …
12 files16 theorems
2024-02-28 16:59 a6f77074
chore: use lt_add_one to simplify proof of exists_abs_lt (#11046)
1 files1 theorems
2024-02-28 16:59 9c5ebcdd
chore: classify `broken dot notation` porting notes (#11038) …
4 files
2024-02-28 16:59 7bd999cc
feat(Data/ZMod/Basic): add some ringEquivCongr API (#11018) …
1 files2 theorems
2024-02-28 16:59 0bbdc654
feat(Mathlib.Topology.Compactness.Compact): add sInter version of Cantor's intersection theorem (#10956) …
11 files5 theorems
2024-02-28 16:59 74460c6f
feat(SetTheory): Upper bound for games (#10566) …
1 files4 theorems
2024-02-28 16:06 bc380937
chore: classify `was decide!` porting notes (#11044) …
6 files
2024-02-28 16:06 295fa276
chore: classify `broken ext` porting notes (#11042) …
2 files
2024-02-28 15:10 cd23c669
chore: remove stream-of-conciousness syntax for `obtain` (#11045) …
48 files
2024-02-28 15:10 866dfe56
refactor: use smul_algebraMap to simply proof of FixedPoints.intermediateField.algebraMap_mem' (#11025) …
1 files
2024-02-28 14:01 1896df51
chore: remove porting notes involving the ematch attribute (#11037) …
2 files
2024-02-28 12:44 30f06274
feat: Laplacian matrix of a simple graph (#8594) …
4 files20 theorems3 defs
2024-02-28 10:54 a66bd9db
chore(Order/Lattice): Resolve porting notes (#11034) …
1 files3 theorems
2024-02-28 10:53 4900a2c5
chore: use mk_pow to simply proof of frobenius_mk (#11024) …
1 files
2024-02-28 10:53 02e43f82
chore: remove AlgHom.coeOutRingHom (#11011) …
1 files
2024-02-28 10:53 9420a7db
chore: remove duplicated namespaces from instances (#10899)
10 files
2024-02-28 10:53 33245d8c
fix: formatting in three authors lines (#10877) …
5 files
2024-02-28 09:50 e69cb643
feat: Unions and intersections indexed by `Finset.sigma` (#10851) …
2 files5 theorems
2024-02-28 08:33 f5e8fa18
feat(LinearAlgebra/TensorProduct): add `TensorProduct.map₂` (#10986)
2 files2 theorems2 defs
2024-02-28 07:39 d6136815
feat(Mathlib/RingTheory/Ideal/QuotientOperations): First Isomorphism Theorem for algebras (#11027) …
2 files2 theorems
2024-02-28 07:04 e059984c
feat: the Fourier transform is self-adjoint (#10833) …
5 files18 theorems3 defs
2024-02-28 00:59 ae9f685e
chore(Algebra/BigOperators): reduce imports for `Multiset.prod` (#10987) …
3 files2 theorems
2024-02-28 00:16 d67e1758
feat: `MeasureSpace` instance on `unitInterval` (#10452) …
3 files6 theorems1 defs
2024-02-27 23:07 fca284d1
feat(Topology/Category): `EffectiveEpi` iff `QuotientMap` in `TopCat` (#10993)
2 files1 theorems1 defs
2024-02-27 23:07 5d73e334
chore(Cauchy): drop `Nonempty`/`Inhabited` assumptions (#10871) …
2 files3 theorems
2024-02-27 22:35 65d37dc6
feat(Algebra/Module/CharacterModule): definition of character module (#10767) …
2 files3 theorems3 defs
2024-02-27 20:35 bb9eaa6b
chore(AlgebraicGeometry.StructureSheaf): remove `erw` (#11022) …
1 files
2024-02-27 19:35 e10b4f54
feat: abstract continuous functional calculus for unital algebras (#5750) …
2 files62 theorems