Changelog

2024-10-22 01:04 cbf4f226
chore: update Mathlib dependencies 2024-10-22 (#18035) …
1 files
2024-10-21 23:17 034f3de5
chore(deps): dependabot updates (#18026) …
16 files
2024-10-21 22:54 ef1ba70e
refactor: merge `ExpChar` and `CharP` API (#18023) …
20 files141 theorems4 defs
2024-10-21 21:50 13d0934b
feat: `‖aba⁻¹b⁻¹ - 1‖ ≤ C ‖a - 1‖ ‖b - 1‖` (#18027) …
1 files4 theorems
2024-10-21 18:56 c3f00b0c
feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions (#16768) …
3 files10 theorems
2024-10-21 16:43 d2c8bedd
chore(Topology/Algebra/SeparationQuotient): split (#18011) …
16 files20 theorems
2024-10-21 16:43 ff8e6e85
feat: semisimple rings are Artinian (#17557) …
7 files6 theorems
2024-10-21 16:18 340899eb
chore(Pointwise/Finset): move `MonoidWithZero` and `Ring` results out (#17999) …
4 files70 theorems
2024-10-21 15:51 e3e46c38
feat: `‖a * b * c‖ ≤ ‖a‖ * ‖b‖ * ‖c‖` (#18005) …
9 files8 theorems
2024-10-21 15:44 0cb54c9f
feat(AlgebraicGeometry): dominant morphisms of schemes (#17961)
3 files6 theorems
2024-10-21 15:16 4ed749a9
RFC chore(GroupTheory/MonoidLocalization): un-`@[simp]` `Localization.mk_eq_monoidOf_mk'` (#18015) …
5 files1 theorems
2024-10-21 15:16 7004cd3f
feat: add missing instances for `ContinuousMap` and `BoundedContinuousFunction` (#17838)
2 files
2024-10-21 14:58 69a4014a
chore(CategoryTheory/Adjunction): homEquiv_unit is no longer a global simp lemma (#17761) …
21 files
2024-10-21 14:44 a60ffdad
chore: add dependabot (#18013) …
1 files
2024-10-21 14:44 d2549910
feat(Data/Real/IsNonarchimedean): add lemmas (#16767) …
5 files17 theorems
2024-10-21 14:11 f4c1fd55
feat: `a ^ n = 1 ↔ n = 0` and similar (#17745) …
2 files6 theorems
2024-10-21 13:21 3bf558f9
feat(Module/ZLattice): define the pullback of a ZLattice (#16822) …
2 files10 theorems2 defs
2024-10-21 10:47 d43bc00b
feat: Popoviciu's inequality (#17868) …
2 files3 theorems
2024-10-21 10:04 1df44a89
chore: remove `CoeFun` instances where `FunLike` is available (#17917) …
2 files
2024-10-21 09:56 ff1b8867
chore: add test to keep powering in `ZMod` fast (#17996) …
1 files
2024-10-21 09:56 59834f40
chore: removed unused variables (#17975) …
18 files
2024-10-21 09:29 355721b6
docs(Computability/EpsilonNFA): typo (#17992) …
1 files
2024-10-21 09:29 336b7469
feat(Topology/Inseparable): add `alias Specializes.of_eq := specializes_of_eq` (#17988) …
1 files
2024-10-21 09:29 5195b1b9
chore(Filter/Tendsto): split from `Basic` (#17959)
11 files116 theorems
2024-10-21 09:29 2edff713
chore(RingTheory/DedekindDomain/FiniteAdeleRing): remove TODO (#17951) …
1 files
2024-10-21 09:29 662a8bae
chore(Data/NNReal): split into `Defs` and `Basic` (#17913) …
10 files280 theorems12 defs
2024-10-21 09:28 8a8d36d5
feat(GroupTheory/Index): index of product of subgroups (#17878) …
1 files2 theorems
2024-10-21 09:28 26449dce
feat(NumberTheory/Ostrowski): Ostrowski's Theorem for the rationals (#17138) …
1 files5 theorems1 defs
2024-10-21 08:47 5958e95e
chore: fix some nits from #12339 (#17994)
2 files
2024-10-21 08:47 3b842b0c
chore: cleanup adaptation notes from 2024-09-06 (#17990)
4 files
2024-10-21 08:28 1404d2bd
feat(ENNReal): liminf/limsup/iInf/iSup and multiplication (#17656) …
3 files8 theorems
2024-10-21 08:12 1fad8e46
feat: the pi sigma-algebra is generated by projections (#17828) …
2 files2 theorems
2024-10-21 07:59 797cd917
chore(ConditionalProbability): review argument implicitness (#17910) …
3 files10 theorems
2024-10-21 06:32 a60b09cd
refactor(SetTheory/Ordinal/Arithmetic): deprecate `blsub₂` (#17679) …
3 files1 theorems
2024-10-21 06:32 f738d222
feat: the multiGoal linter (#12339) …
8 files2 defs
2024-10-21 05:53 c8f7de85
chore: move batteries back to main; bump (#17991) …
2 files
2024-10-21 03:20 4d87f692
chore: rename List.modifyNth->modify and insertNth->insertIdx (#17985) …
15 files70 theorems2 defs
2024-10-21 01:17 34309b69
chore(build.in): update version of `gh-get-current-pr` action (#17978) …
4 files
2024-10-21 01:17 4f5e6c17
feat(Data/Nat/Bitwise): add simp lemmas (#17977) …
1 files2 theorems
2024-10-21 00:40 a9827c1f
feat(Data/Set/Basic): add `diff_insert_of_not_mem` (#17973) …
1 files1 theorems
2024-10-21 00:31 0cfd3c80
chore: more fixes for multigoal linter (#17966) …
8 files
2024-10-20 21:50 69bbcb4a
chore: move `mul_ite`, add `dite` version, multiplicativise `ite_add_ite` (#17963)
2 files16 theorems
2024-10-20 21:29 1b6c758c
feat: `negOnePow n = (-1 : ℤ) ^ n` (#17967) …
2 files4 theorems
2024-10-20 19:54 cf0049ec
feat(CategoryTheory): natural version of `FullyFaithful.homEquiv` (#17450)
1 files2 defs
2024-10-20 19:39 a3996466
feat(Analysis/Normed/Field/Ultra): nonarchimedean iff norm of nats le one (#15077)
2 files5 theorems
2024-10-20 18:58 15fb8246
chore(Topology/Exterior): golf (#17955) …
1 files3 theorems
2024-10-20 17:40 03a37e0b
chore(LinearAlgebra/TensorProduct): fix duplication (#17912) …
2 files1 theorems
2024-10-20 16:57 8d27fbf3
feat(CategoryTheory): pull colimits out of hom functors with Yoneda on the LHS (#17440) …
2 files1 theorems
2024-10-20 13:29 0dedd92e
chore: Rename `ClosedEmbedding` to `IsClosedEmbedding` (#17937) …
83 files166 theorems2 structures
2024-10-20 13:19 e7b15d2c
feat(Analysis/Complex/Positivity): new file (#17862) …
3 files8 theorems