Changelog
2024-12-20 23:22 5ba284dd
feat(FieldTheory/Galois): Fundamental theorem of infinite galois theory (#16982) …
3 files8 theorems3 defs
2024-12-20 22:56 2f2de82a
feat(DiscreteValuationRing/Basic): a ring equivalent to a DVR is a DVR (#20073) …
1 files1 theorems
2024-12-20 22:32 31e1a94c
feat(RingTheory/Flat): generalize `flat_of_isLocalized_span` (#19788) …
7 files15 theorems1 defs
2024-12-20 20:23 75faccb7
feat: some more properties of linearly disjoint (#19614) …
5 files41 theorems3 defs
2024-12-20 20:04 3bc257ba
feat(GroupTheory/SemidirectProduct): Add various maps (#20102) …
1 files11 theorems6 defs
2024-12-20 19:39 1a3f2a10
feat(GroupTheory/Transfer): A cyclic Sylow subgroup for the smallest prime has a normal complement (#19587) …
2 files3 theorems
2024-12-20 17:17 74c027f0
feat(Algebra/Homology): the stupid truncation of homological complexes (#18501)
4 files5 theorems
2024-12-20 17:08 7f72da4f
feat(CategoryTheory): the left lifting property is stable under transfinite composition (#20119) …
2 files6 theorems2 defs1 structures
2024-12-20 16:26 75d219b4
chore: rename `coeff_modByMonic_mem_span_pow_mul_span` (#20118)
1 files4 theorems
2024-12-20 16:26 fcdc29cb
doc(1000.yaml): add entries for 100 theorems (#20114) …
2 files
2024-12-20 16:26 2a41753e
feat(GroupTheory/SpecificGroups/Cyclic): Add `isCyclic_of_injective` (#20103) …
1 files2 theorems
2024-12-20 16:26 fa580ede
feat: isomorphic rings have isomorphic spectra (#20068) …
1 files3 theorems1 defs
2024-12-20 16:26 9cc15b97
feat(CategoryTheory/Sites): colimits in categories of extensive sheaves are computed objectwise (#19913) …
4 files1 theorems1 defs
2024-12-20 16:26 e234a9fb
feat(CategoryTheory): infer connectedness of comma categories from finality/initiality of the functor (#19889)
3 files4 theorems
2024-12-20 16:26 128a213e
feat(RingTheory): `AlgebraicIndependent` persists to `algebraicClosure` (#19708) …
4 files11 theorems
2024-12-20 16:06 e5c7795a
feat: Define ENorm notation class (#20121) …
3 files34 theorems2 defs2 structures
2024-12-20 15:50 f9d7e617
chore(ModelTheory): fix docstring (#20116)
1 files
2024-12-20 15:50 53defdf1
feat(Algebra/Module): presentation of the tensor product (#18432) …
2 files1 theorems
2024-12-20 15:50 b95ee76f
feat(Algebra/Category/ModuleCat): the pseudofunctors which send a ring to its category of modules (#18197) …
3 files12 theorems
2024-12-20 15:29 ea4f170a
doc(100,1000.yaml): tweak resp. add entry for Cantor's diagonal argument (#20112) …
2 files
2024-12-20 15:29 7987fe32
doc(*.yml): mention Sylow theorems (#20111) …
4 files
2024-12-20 15:29 2fbbcf1d
feat: the successor as a function `WithBot α → α` (#20055) …
5 files26 theorems2 defs
2024-12-20 15:29 92c2d0cb
feat(CategoryTheory/Enriched): functoriality of the enrichment of functor categories (#18414) …
1 files1 theorems
2024-12-20 14:57 81263905
feat: iUnion and iInter over PSigma (#20077)
1 files4 theorems
2024-12-20 14:57 a4cfef87
feat: determinant of left multiplication (#19873) …
2 files4 theorems
2024-12-20 14:36 42764fbc
chore: generalise `‖a ^ n‖ ≤ n * ‖a‖` to non-abelian groups (#20110) …
3 files2 theorems
2024-12-20 14:09 83682ff2
feat(RingTheory): the residue field of a prime ideal (#18416)
2 files6 theorems1 defs
2024-12-20 13:13 49f1292b
chore: move `Logic.Equiv.TransferInstance` to `Algebra.Equiv.TransferInstance` (#19993)
20 files
2024-12-20 13:13 4649cb13
chore: split material about continued fractions from DiophantineApproximation (#19820)
4 files4 theorems
2024-12-20 13:13 4bbcfacc
feat(RingTheory): `HomogeneousLocalization.awayMap` is a localization (#19486) …
2 files4 theorems
2024-12-20 13:13 949bc42a
feat(CategoryTheory/MorphismProperty): classes of morphisms that are stable under transfinite compositions (#19306)
3 files4 theorems2 defs1 inductives
2024-12-20 13:13 ef7c8b7a
refactor(Nat.Prime.Defs): use `csimp` for `Nat.decidablePrime` (#19240) …
1 files1 theorems2 defs
2024-12-20 13:13 733489d6
feat: add `ENat.map` and lemmas (#19149)
4 files11 theorems2 defs
2024-12-20 13:13 c800d7a3
feat(Data/Nat/Nth): `nth_add_one` (#18836) …
1 files5 theorems
2024-12-20 13:13 69d5dbc0
feat(Algebra/MvPolynomial): Schwartz-Zippel lemma (#5297) …
3 files3 theorems
2024-12-20 12:30 486b7112
chore(GodelBetaFunction): use `getElem` (#20105)
1 files1 theorems
2024-12-20 12:30 0719ca8f
chore: rename List.Vector.get_eq_get (#20087)
3 files2 theorems
2024-12-20 12:30 02bf40fb
feat: monovarying functions are simultaneously monotone (#20047) …
2 files8 theorems1 defs
2024-12-20 12:30 02abf1b4
chore: revert import order between Algebra.Group.ZeroOne and Logic.Nonempty (#19994)
11 files2 theorems
2024-12-20 12:30 83450e8f
chore: tidy various files (#17342)
30 files3 theorems
2024-12-20 12:18 5ba57828
feat(Algebra/Category/Ring): Tensor product over Z is coproduct in `CommRingCat` (#19976) …
1 files2 theorems3 defs
2024-12-20 12:02 e5485b24
feat(Valued/LocallyCompact): `totallyBounded_iff_finite_residueField` (#15424)
3 files14 theorems
2024-12-20 11:52 772472af
feat: `aeval` a Chebyshev polynomial (#19952) …
2 files16 theorems
2024-12-20 11:33 5465191d
feat(GroupTheory/Index): Add `Subgroup.card_range_dvd` and `Subgroup.card_map_dvd` (#20100) …
1 files2 theorems
2024-12-20 11:33 7c2ef337
chore(IsAlgClosed/Classification): make theorems more universe polymorphic (#18434)
2 files7 theorems
2024-12-20 11:24 a7ed2d05
refactor(GroupTheory/SpecificGroups/Cyclic): Add `isCyclic_iff_exists_zpowers_eq_top` and golf (#20085) …
1 files4 theorems
2024-12-20 10:20 78a1c375
feat(RingTheory/Ideal/Over): define the set of all prime ideals that lie over an ideal (#19139) …
4 files11 theorems1 defs
2024-12-20 10:20 25ee8b01
feat(Algebra/Order/Monoid/Unbundled/WithTop): add lemmas about `WithTop.map` and `WithBot.map` (#19122)
2 files20 theorems
2024-12-20 09:05 d70be405
refactor(Algebra/Group/Subgroup/Basic): Rename `normalizer_eq_top` to `normalizer_eq_top_iff` (#20109) …
6 files2 theorems
2024-12-20 09:05 31a16b3f
feat(GroupTheory/Solvable): Prove `isSolvable_iff_commutator_lt` (#20107) …
1 files3 theorems