Changelog

2024-04-15 21:55 ca1a851a
chore: fix topic name in nightly-testing bot (#12165)
1 files
2024-04-15 19:14 b0fff6f5
chore: rename `StarOrderedRing` convenience constructors (#12089) …
3 files6 theorems
2024-04-15 15:25 bec5207f
refactor(RingTheory.MvPolynomial.Homogeneous): refactor in terms of weightedHomogeneous (#7609) …
2 files18 theorems5 defs
2024-04-15 14:21 28bea03d
refactor(Rat): Streamline basic theory (#11504) …
20 files66 theorems10 defs
2024-04-15 13:31 9125a093
feat(Algebra/Lie): define adjoint action and its ideal image (#12106) …
5 files6 theorems2 defs
2024-04-15 12:36 b8a0f589
chore: avoid id.def (adaptation for nightly-2024-03-27) (#11829)
75 files
2024-04-15 12:06 8a7f8422
chore: remove remaining `cdot`s that were not `·` (#12146) …
2 files
2024-04-15 10:00 4932e9d1
chore(Topology/Category): make finite coproducts in `CompHaus` universe polymorphic (#12138)
2 files2 theorems1 defs
2024-04-15 10:00 7700a474
Feat(Log/Base): Adding 3 theorems related to Real.logb (#12110)
1 files3 theorems
2024-04-15 09:36 91ab481b
chore: don't run label_new_contributor CI on forks (#12145)
1 files
2024-04-15 08:19 8e47cfa4
chore(GroupAction/Defs): add 2 missing `to_additive` (#12141)
1 files
2024-04-15 08:19 6b1d0a88
chore: fixed typo in Algebra.Homology.HomotopyCategory (#12140) …
1 files
2024-04-15 08:19 f09078b7
chore: remove more simp-related porting notes which are fixed now (#12128)
6 files
2024-04-15 07:51 5894eb31
refactor(Topology): take continuous argument in `LocallyConstant.comap` (#12136) …
5 files8 theorems4 defs
2024-04-15 06:46 88ce0991
chore: substitute some `.` with `·` (#12137)
13 files1 theorems
2024-04-15 06:46 7eeaaffb
chore: classify porting notes about additional necessary beta reduction (#12130) …
16 files1 defs
2024-04-15 06:46 038cb584
refactor(SpecialFunctions/Gaussian): shorten long pole (#12104) …
12 files112 theorems2 defs
2024-04-15 06:22 7c5b29b7
chore: restore `simp`s that used to work (#12126)
8 files
2024-04-15 03:03 5d492760
feat(Profinite): the functors from `FintypeCat` are fully faithful (#12139) …
2 files
2024-04-15 01:53 d48d30ac
chore: superfluous parentheses part 2 (#12131)
243 files1 defs
2024-04-14 18:26 22092a2a
chore(RingTheory/FinitePresentation): make `Algebra.FinitePresentation` a class (#12057) …
1 files6 theorems1 defs
2024-04-14 14:15 8a48cc6b
refactor(LinearAlgebra/BilinearForm/Basic): Deprecate coercions (#12132) …
2 files1 theorems
2024-04-14 13:46 94e622af
feat(RingTheory/Kaehler): The Kaehler differential module of polynomial algebras. (#11895)
3 files11 theorems3 defs
2024-04-14 12:41 db53e50d
feat(NumberTheory/ModularForms): Asymptotics of Jacobi theta functions (#12020) …
10 files16 theorems5 defs
2024-04-14 10:41 9e99a83e
doc: fix references to List.Pairwise in List.Sorted docs (#12123)
1 files
2024-04-14 10:41 9e512a0a
refactor(LinearAlgebra/BilinearForm/Basic): Delete infered instances (#12122) …
1 files
2024-04-14 10:41 3bb1d613
chore: remove autoImplicit from more files (#11798) …
54 files115 theorems14 defs
2024-04-14 10:02 97558f9c
chore: make instSMulRealComplex scoped (#12080) …
3 files
2024-04-14 09:14 60650e90
feat(CategoryTheory/CommSq): add basic CommSq lemmas (#12033) …
1 files3 theorems
2024-04-14 08:49 f822da54
feat(NumberTheory/SmoothNumbers): add material on numbers with prime factors in a given Finset (#12055) …
1 files19 theorems2 defs
2024-04-14 07:43 1ef4afc1
chore(Algebra/BigOperators): delete `RingHom.map_*` lemmas (#11663)
7 files
2024-04-14 06:35 02b6c2be
chore(*Set): golf (#12117) …
4 files
2024-04-14 06:35 596d5eca
chore: superfluous parentheses (#12116)
28 files
2024-04-14 05:44 79d6c97c
feat(LinearAlgebra/TensorProduct/Finiteness): add some finiteness results of tensor product (#11859) …
3 files12 theorems
2024-04-13 20:23 9670eb9f
feat: Inverses for TrivSqZeroExt (#12075) …
2 files4 theorems
2024-04-13 19:32 7e8cd2b7
feat(Data/Nat/Prime): add 2 theorems (#11620)
1 files4 theorems
2024-04-13 18:06 a0cb217e
fix(Algebra/Bounds): generalize index type to sort (#12113)
1 files
2024-04-13 12:00 7a71e528
Feat (GroupTheory/GroupAction/Hom/Pointwise) : generalize smul set lemmas to group actions (#12023) …
4 files16 theorems
2024-04-13 10:35 8640948c
feat: add notation for Real.sqrt (#12056) …
51 files127 theorems3 defs
2024-04-13 10:35 51eea185
feat: generalize integration by parts (#11886) …
2 files9 theorems
2024-04-13 10:09 4d302c53
adding `Functor.sum'`, dual to `Functor.prod'`. (#12073) …
1 files3 defs
2024-04-13 09:22 fef3b89b
chore: resolve some simp-related porting notes (#12074) …
12 files
2024-04-13 04:55 c411fe2e
chore(Data/Set/Intervals/OrdConnectedComponent): resolve porting note about lift not being … (#12102) …
1 files
2024-04-13 04:55 33c3101f
chore: remove porting notes about redundant binder updates (#12101) …
7 files
2024-04-13 04:55 c5b5490c
chore: classify porting notes referring to missing linters (#12098) …
116 files
2024-04-13 04:55 203c0592
chore(RingTheory/Ideal/Cotangent): Restore lemmasOnly config on `Ideal.toCotangent`. (#12088)
2 files
2024-04-13 04:55 667acd1e
chore(Algebra/Ring/Int): add `CharZero` instance for `Int` (#12060) …
6 files
2024-04-13 04:26 38a23fcc
chore(RingTheory/IsTensorProduct): resolve porting note about simps! (#12092) …
1 files1 theorems
2024-04-12 23:11 cd0e7a0d
chore(Data/Finset/PiInduction): remove porting note about `clear_value` (#12100) …
1 files
2024-04-12 19:06 72721e37
fix: mdata in abel (#12084) …
2 files