Changelog
2024-10-29 02:02 3e82c092
feat: lemma concerning for `‖cfc f a‖ < c` (#18361)
1 files12 theorems
2024-10-29 01:28 06988e96
chore: remove a few unused variables (#18362) …
3 files
2024-10-29 00:42 ef637a3d
fix(LongestPole): windows paths compatibility (#18341) …
1 files
2024-10-29 00:06 a3fa624c
feat: `cfc_tsub` for `ℝ≥0` functions (#18360)
1 files2 theorems
2024-10-28 23:09 d57b21ae
refactor(RingTheory/Ideal/Pointwise): Generalize to semirings (#18355) …
2 files2 theorems
2024-10-28 20:59 1d847d8c
feat(CategoryTheory) : (Co)structured arrow as a functor to Cat (#18298) …
2 files5 defs
2024-10-28 20:27 d131995e
feat(RingTheory/IsLasker): strength primary decomposition to a minimal one (#18296) …
4 files11 theorems1 defs
2024-10-28 20:08 2d770eb4
feat(RingTheory): generalize `Ideal.IsPrimary` to submodules (#17073) …
6 files6 theorems1 defs
2024-10-28 18:56 a4ea5875
chore: update Mathlib dependencies 2024-10-28 (#18350) …
1 files
2024-10-28 17:42 4e5fa637
chore(Algebra/Group/Subgroup): split off `Defs` file (#18340) …
21 files144 theorems16 defs12 structures
2024-10-28 16:16 97a2bd10
doc(Analysis/RCLike/Basic): correct link in documentation (#18343)
1 files
2024-10-28 15:52 91c49567
feat(Topology) define jacobson spaces (#18243)
3 files13 theorems1 defs
2024-10-28 15:52 8781866c
feat(Algebra/FreeMonoid): set of symbols appearing in an element of the free monoid (#18036) …
2 files4 theorems1 defs
2024-10-28 15:52 31142eae
feat(Archive/Imo): formalize IMO 1982q1 (#16883) …
2 files9 theorems1 structures
2024-10-28 15:32 3195aa05
feat(NumberField/CanonicalEmbedding): define the `negAt` map (#18234) …
3 files17 theorems4 defs
2024-10-28 15:32 c0749f64
feat: matrices with fixed determinant (#16159) …
3 files5 theorems1 defs
2024-10-28 15:32 04cd6e34
feat(RingTheory/Flat): faithfully flat ring maps (#15014) …
1 files6 theorems
2024-10-28 14:59 afa7411c
chore: remove almost all `import Lean` (#18276) …
37 files
2024-10-28 14:43 3c6a5802
chore: remove unused vars (#18337) …
12 files
2024-10-28 14:43 2c754340
chore(CategoryTheory/Functor): dualize `OfSequence` (#18325)
1 files1 theorems2 defs
2024-10-28 14:43 41221c61
feat(AlgebraicGeometry/PrimeSpectrum): prime spectrum of jacobson rings (#18242)
4 files8 theorems
2024-10-28 14:12 fb0124bc
feat: `a / b < 0 → 0 ≤ a → b < 0` (#18260)
1 files5 theorems
2024-10-28 13:54 4cfaaae1
feat: `EReal.forall`, `EReal.exists` (#18301)
1 files
2024-10-28 13:47 0610ff0c
doc: fix typo in perfect numbers module docstring (#18334)
1 files
2024-10-28 13:33 ed81cec6
feat(Algebra/Module): presentation of modules (#18295) …
2 files26 theorems2 defs4 structures
2024-10-28 13:23 997f6e38
chore: remove some `maxHeartbeats` bumps that are no longer needed (#18324) …
5 files
2024-10-28 13:03 e43d3141
feat: indicator of a clopen set as a bounded continuous function (#18291) …
2 files
2024-10-28 12:34 73c9a638
chore: remove more variables (#18323) …
33 files
2024-10-28 11:34 2d2bbe0b
chore: cleanup skipAssignedInstances flags (#18320)
12 files
2024-10-28 10:57 d886d6dd
feat: add by how many modules imports grew (#18303) …
2 files2 defs1 structures
2024-10-28 10:31 992d67f3
feat(Algebra/Order/Field/Basic): add Nat cast lemmas (#18171) …
1 files3 theorems
2024-10-28 09:52 f381acde
chore: remove some no-longer-needed backwards compatibility flags (#18319)
3 files
2024-10-28 09:52 f043a235
feat: lake exe unused (#18156) …
8 files10 defs1 structures
2024-10-28 09:08 38a786e8
chore: some `erw`s that can become `rw` for free (#18322) …
1 files
2024-10-28 09:08 63796b69
chore: move contents of Data.Finite.Basic earlier (#18316)
10 files
2024-10-28 09:08 73203f9a
chore: import Mathlib.Init in all files (#18277) …
16 files4 theorems
2024-10-28 09:08 fb052069
feat(RingTheory/Ideal/Maps): lemmas of ring isomorphisms act on ideals (#18249) …
2 files7 theorems
2024-10-28 09:08 bacb7f7d
feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) (#17820) …
2 files35 theorems
2024-10-28 08:46 a9ecf75b
chore: Rename `Embedding` to `IsEmbedding` (#18133) …
105 files206 theorems2 defs4 structures
2024-10-28 08:12 5741a44f
chore(Data/List): move the definition of finRange to Defs (#18312)
3 files2 defs
2024-10-28 08:12 f717d6ab
feat: `ext` lemmas for `MultilinearMap` (#18308) …
2 files2 theorems
2024-10-28 08:12 c9cc2f63
chore: remove unused variables (#18305) …
28 files
2024-10-28 08:12 efd9ebb8
chore(Wiedijk100Theorems): clean up SolutionToCubic (#18299) …
2 files3 theorems
2024-10-28 07:22 9fc60c1a
feat: `ZMod`-module lemmas (#17693) …
1 files8 theorems
2024-10-28 06:12 deda35aa
chore: split Data.Set.Basic (#18317) …
15 files16 theorems
2024-10-28 06:12 091df8ec
chore: split Mathlib.Topology.Algebra.UniformGroup (#18311) …
17 files82 theorems2 defs
2024-10-28 06:12 f4eb221a
feat: gluing measurable functions along measurable embeddings (#18287)
1 files4 theorems
2024-10-28 06:12 95c5f3f5
refactor: generalize AddSubmonoid Mul lemmas to SMul (#18278)
3 files6 theorems
2024-10-28 06:12 b8b4846e
feat(Algebra/Polynomial/AlgebraMap): add `algEquiv(OfCompEqX|AevalXAddC)_(eq_iff|symm)` (#18257)
1 files4 theorems
2024-10-28 06:12 4d43a68b
feat(FieldTheory): define induced action of subfields and intermediate fields (#18141) …
2 files2 theorems