Changelog

feat(FieldTheory/Galois): Fundamental theorem of infinite galois theory (#16982) …

feat(DiscreteValuationRing/Basic): a ring equivalent to a DVR is a DVR (#20073) …

feat(RingTheory/Flat): generalize `flat_of_isLocalized_span` (#19788) …

feat: some more properties of linearly disjoint (#19614) …

feat(GroupTheory/SemidirectProduct): Add various maps (#20102) …

feat(GroupTheory/Transfer): A cyclic Sylow subgroup for the smallest prime has a normal complement (#19587) …

feat(Algebra/Homology): the stupid truncation of homological complexes (#18501)

feat(CategoryTheory): the left lifting property is stable under transfinite composition (#20119) …

chore: rename `coeff_modByMonic_mem_span_pow_mul_span` (#20118)

doc(1000.yaml): add entries for 100 theorems (#20114) …

feat(GroupTheory/SpecificGroups/Cyclic): Add `isCyclic_of_injective` (#20103) …

feat: isomorphic rings have isomorphic spectra (#20068) …

feat(CategoryTheory/Sites): colimits in categories of extensive sheaves are computed objectwise (#19913) …

feat(CategoryTheory): infer connectedness of comma categories from finality/initiality of the functor (#19889)

feat(RingTheory): `AlgebraicIndependent` persists to `algebraicClosure` (#19708) …

feat: Define ENorm notation class (#20121) …

chore(ModelTheory): fix docstring (#20116)

feat(Algebra/Module): presentation of the tensor product (#18432) …

feat(Algebra/Category/ModuleCat): the pseudofunctors which send a ring to its category of modules (#18197) …

doc(100,1000.yaml): tweak resp. add entry for Cantor's diagonal argument (#20112) …

doc(*.yml): mention Sylow theorems (#20111) …

feat: the successor as a function `WithBot α → α` (#20055) …

feat(CategoryTheory/Enriched): functoriality of the enrichment of functor categories (#18414) …

feat: iUnion and iInter over PSigma (#20077)

feat: determinant of left multiplication (#19873) …

chore: generalise `‖a ^ n‖ ≤ n * ‖a‖` to non-abelian groups (#20110) …

feat(RingTheory): the residue field of a prime ideal (#18416)

chore: move `Logic.Equiv.TransferInstance` to `Algebra.Equiv.TransferInstance` (#19993)

chore: split material about continued fractions from DiophantineApproximation (#19820)

feat(RingTheory): `HomogeneousLocalization.awayMap` is a localization (#19486) …

feat(CategoryTheory/MorphismProperty): classes of morphisms that are stable under transfinite compositions (#19306)

refactor(Nat.Prime.Defs): use `csimp` for `Nat.decidablePrime` (#19240) …

feat: add `ENat.map` and lemmas (#19149)

feat(Data/Nat/Nth): `nth_add_one` (#18836) …

feat(Algebra/MvPolynomial): Schwartz-Zippel lemma (#5297) …

chore(GodelBetaFunction): use `getElem` (#20105)

chore: rename List.Vector.get_eq_get (#20087)

feat: monovarying functions are simultaneously monotone (#20047) …

chore: revert import order between Algebra.Group.ZeroOne and Logic.Nonempty (#19994)

chore: tidy various files (#17342)

feat(Algebra/Category/Ring): Tensor product over Z is coproduct in `CommRingCat` (#19976) …

feat(Valued/LocallyCompact): `totallyBounded_iff_finite_residueField` (#15424)

feat: `aeval` a Chebyshev polynomial (#19952) …

feat(GroupTheory/Index): Add `Subgroup.card_range_dvd` and `Subgroup.card_map_dvd` (#20100) …

chore(IsAlgClosed/Classification): make theorems more universe polymorphic (#18434)

refactor(GroupTheory/SpecificGroups/Cyclic): Add `isCyclic_iff_exists_zpowers_eq_top` and golf (#20085) …

feat(RingTheory/Ideal/Over): define the set of all prime ideals that lie over an ideal (#19139) …

feat(Algebra/Order/Monoid/Unbundled/WithTop): add lemmas about `WithTop.map` and `WithBot.map` (#19122)

refactor(Algebra/Group/Subgroup/Basic): Rename `normalizer_eq_top` to `normalizer_eq_top_iff` (#20109) …

feat(GroupTheory/Solvable): Prove `isSolvable_iff_commutator_lt` (#20107) …