Changelog

2024-06-18 00:39 1db89cb5
feat: add definition of opposite of subsemirings, subrings, and subalgebras (#12846) …
4 files86 theorems12 defs
2024-06-17 21:56 ae4167de
feat: technical debts compare to previous week (#13892) …
3 files
2024-06-17 21:56 27c7d55a
chore: use `SemilinearMapClass` in `Module.Finite.range` (#13863) …
1 files
2024-06-17 20:45 b83d79b9
fix(GetAllModules): sort module names instead of file names (#13854) …
2 files2 defs
2024-06-17 20:45 13d4164a
fix(test/Lint.lean): re-enable test for duplicate namespaces (#13670) …
2 files2 defs
2024-06-17 20:45 5b624694
feat(NumberTheory/PrimeCounting): Lemma: The `n`th prime is greater or equal `n + 2`. (#13283) …
0 files
2024-06-17 22:37 72d08e5f
feat(NumberTheory/PrimeCounting): Lemma: The `n`th prime is greater or equal `n + 2`. (#13283) …
2 files2 theorems
2024-06-17 18:49 11fae86a
feat(RingTheory/Congruence): split `RingCon` construction and add some constructions (#13730) …
6 files2 theorems3 defs
2024-06-17 16:57 009daa3a
feat: positivity of `star x * x` (#13748) …
3 files6 theorems
2024-06-17 16:07 b9b6c25c
feat(EllipticCurve): a coordinate ring over a domain is a domain (#12883) …
1 files3 theorems
2024-06-17 16:07 459cd285
feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): compute degrees of division polynomials (#10878)
3 files15 theorems
2024-06-17 15:40 12613ba8
chore(Analysis/Normed/Group): Move constructions (#13894) …
7 files86 theorems
2024-06-17 15:04 739a018e
feat(Algebra/Lie/Normalizer): add `normalizer_mono` and use it to fix a porting note (#13890) …
2 files2 theorems
2024-06-17 14:41 57aa9c9a
feat(CategoryTheory/Category/Cat): add Cat API (#13809) …
1 files8 theorems
2024-06-17 14:29 402ae165
feat(CategoryTheory): characterise the covering sieves for the extensive topology (#13897)
5 files5 theorems2 defs
2024-06-17 13:58 bb514bfc
docs(CategoryTheory): improve documentation in the effective epi file (#13805) …
1 files
2024-06-17 11:31 bdd39e92
feat(Data/Fintype/Basic): `Finset.univ_map_subtype` lemmas (#12903) …
1 files3 theorems
2024-06-17 11:20 e6faccc1
chore(NumberTheory/MulChar): deprecate `IsNontrivial`, fix `isPrimitive` (#13878) …
7 files23 theorems3 defs
2024-06-17 10:24 4c302e76
feat(Tactic/Relation/Trans): trans tactic for implications (#13719) …
2 files1 defs1 inductives
2024-06-17 10:24 217718fb
feat: `(𝓝[<] x).NeBot` instances for `Prod`, `Pi`, `OrderDual` (#13642)
5 files5 theorems
2024-06-17 08:52 9cbd6ff1
feat: add missing WithTop/WithBot lemmas and improve WithBot Nat proofs (#13884)
3 files10 theorems
2024-06-16 23:25 77e1ea0a
feat: `Prod.fst` as a lattice hom (#13830) …
1 files6 theorems3 defs
2024-06-16 20:27 782e4af4
chore(HashMap): deprecate unused API additions (#13746)
1 files
2024-06-16 19:40 f2405442
doc(Tactic/Linarith): update docs (#13856) …
8 files
2024-06-16 19:40 acdc9041
chore: Golf `Finset.prod_ite_of_true` (#13726) …
4 files8 theorems
2024-06-16 19:40 6e0b6297
feat(Finset/Lattice): add `Finset.sup_eq_top_iff` etc (#13641)
1 files1 theorems
2024-06-16 19:40 f246e5b7
feat: format table (#12322) …
3 files2 defs1 inductives
2024-06-16 19:19 43431072
chore(MeasureTheory): remove remaining use of autoImplicit true (#13870)
4 files5 theorems
2024-06-16 18:56 d2d320bc
feat: absolute continuity, Radon-Nikodym derivatives of `μ.map f` for a measurable embedding `f` (#13761)
5 files9 theorems
2024-06-16 15:16 d394d9f4
chore(NumberTheory/MulChar): fix `Fintype`/`Finite`, generalize (#13862) …
1 files2 theorems
2024-06-16 14:17 7e44b8f0
feat(Set/Image): add 2 lemmas (#13592) …
1 files2 theorems
2024-06-16 14:17 d476d23a
feat(Topology): some lemmas about continuity of maps out of one point compactifications (#13355) …
1 files3 theorems3 defs
2024-06-16 13:53 dddafd1d
chore(Module/StrongTopology): drop unused `variable`s (#13666)
1 files
2024-06-16 12:04 950e3d06
feat (MeasureTheory/Function): trivial cases of integrability / summability (#13872) …
2 files3 theorems
2024-06-16 11:38 0c9132ba
feat: `a ^ (p - 1) = if a ≠ 0 then 1 else 0` in `ZMod p` (#13828) …
1 files1 theorems
2024-06-16 10:23 895010aa
feat: `1 ≤ s.card ↔ s.Nonempty` (#13821) …
2 files3 theorems
2024-06-16 06:51 f47614aa
chore: implement final style feedback from #13176 (#13865) …
1 files
2024-06-16 06:37 59c05f4a
perf(MeasureTheory,Probability): expand slow `measurabilty` calls (#13770) …
7 files
2024-06-16 11:45 46b526ec
chore: updates for new dsimpNF linter (#13855) …
10 files
2024-06-15 22:45 7dc413fe
chore: Fix statement of `Finset.sum_boole_mul` (#13825) …
1 files
2024-06-15 21:43 32cac551
chore: tidy various files (#13860)
37 files3 theorems
2024-06-15 21:43 a1210a98
feat: `a * (b - 1) = a * b - a` for truncated subtraction (#13826) …
5 files6 theorems
2024-06-15 21:43 48de726c
feat: `norm_cast` lemmas about `IsSquare` and `{Int,Rat}.sqrt` (#13788)
4 files11 theorems
2024-06-15 21:43 0e39a68f
A ring homomorphism ``f : R →+* S`` induces a homomorphism ``GLₙ(f) : GLₙ(R) →* GLₙ(S)``. (#13768)
1 files3 theorems1 defs
2024-06-15 21:09 0ac1ced0
feat: weaken 2nd countable to lindelof in Regular+Lindelof=>Normal (#13176)
4 files7 theorems1 defs
2024-06-15 18:23 03092720
feat(Linter): enforce `since :=` fields in `@[deprecated]` (#13678)
1 files1 defs
2024-06-15 16:49 a9fbabf8
feat(GroupWithZero): add one_lt_coe and friends (#13853)
1 files4 theorems
2024-06-15 15:52 7f2007a3
chore(*): more `since :=` in `deprecated` (#13723)
23 files2 theorems
2024-06-15 14:58 e956397c
chore(*): more `since :=` in `deprecated` (#13839)
45 files6 theorems2 defs
2024-06-15 13:54 90b6f6d9
feat: include `tactic.skipAssignedInstances` flags in technical debt counters (#13851) …
1 files