feat(Condensed): light condensed objects #9515

and a few more lemmas. From LeanAPAP

I suspect I will need some of these for #10660

`ball` for "bounded forall" and `bex` for "bounded exists" are from experience very confusing abbreviations. This PR renames them to `forall_mem` and `exists_mem` in the few `Set` lemma names that mention them. Also deprecate `ball_image_of_ball`, `mem_image_elim`, `mem_image_elim_on` since those lemmas are duplicates of the renamed lemmas (apart from argument order and implicitness, which I am also fixing by making the binder in the RHS of `forall_mem_image` semi-implicit), have obscure names and are completely unused.

Classifies by adding issue number #11215 to porting notes claiming "TODO".

Classifies by adding issue number #10756 to porting notes claiming anything semantically equivalent to: - "new lemma" - "added lemma"

…orm (#11078) Replaces `BilinForm` with `LinearMap.BilinForm` in support of #10553

From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.

…es of `PiTensorProduct` (#11152) * Prove some properties of `PiTensorProduct.map`, for example the compatibility with composition and reindeixing, and the fact that it sends the identity to the identity. * Construct `PiTensorProduct.map` as a `MultilinearMap` on the family of linear maps. * Upgrade `PiTensorProduct.map f` to a linear equivalence called `PiTensorProduct.congr f` when `f` is a family of linear equivalences. * For `ι` a `Fintype`, define the canonical linear equivalence (given by multiplication) `constantBaseRingEquiv` from `⨂ i : ι, R` and `R`. Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Introduces a new class, `PerfectSpace`, which requires that `Set.univ` is a perfect set. This is equivalent to say that no points are isolated (`perfectSpace_iff_forall_not_isolated`).

…0902) See [Zulip chat](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Is.20there.20a.20name.20for.20.22closure.20is.20the.20union.20of.20.60Specializes.60.22.3F)

…e essentially surjective (#11239) Show that if `F.obj` is surjective, `F` is essentially surjective.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

This PR accompanies #11246, squeezing some non-terminal `simp`s highlighted by the linter until I decided to stop!

Classifies by adding issue number #11224 to porting notes claiming: > change `rw` to `erw`

Classifies by adding issue number #11227 to porting notes claiming anything equivalent to: - "added `dsimp`" - "`dsimp` added" - "`dsimp` now needed"

Classifies by adding issue number #11229 to porting notes claiming: > deprecated

Add `tendsto_of_integral_tendsto_of_monotone`, as well as `...of_antitone` and the corresponding results for `lintegral`. Also: - move some results about measurability of limits of (E)NNReal valued functions from BorelSpace.Metrizable to BorelSpace.Basic to make them available in Integral.Lebesgue. - add `lintegral_iInf'`, a version of `lintegral_iInf` for a.e.-measurable functions. We already have the corresponding `lintegral_iSup'`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

…6262) This PR removes the default values for `nsmul` and `zsmul`, forcing the user to populate them manually. The previous behavior can be obtained by writing `nsmul := nsmulRec` and `zsmul := zsmulRec`, which is now in the docstring for these fields. The motivation here is to make it more obvious when module diamonds are being introduced, or at least where they might be hiding; you can now simply search for `nsmulRec` in the source code. Arguably we should do the same thing for `intCast`, `natCast`, `pow`, and `zpow` too, but diamonds are less common in those fields, so I'll leave them to a subsequent PR. Co-authored-by: Matthew Ballard <matt@mrb.email>

Resolves porting notes claiming "change `(coe : ℤ → α)` to `((↑) : ℤ → α)`" by substituting `Int.cast` with `(↑)`.

This adds instances of the continuous functional calculus for unital C⋆-algebras for normal, selfadjoint, and positive elements.

Release 4.7.0-rc1 makes it unnecessary to add `pp_dot` to structure fields. It used to be that function fields wouldn't pretty print using dot notation when the function was applied unless `pp_dot` was added.

This is not exhaustive; it largely does not rename instances that relate to algebra, and only focuses on the "core" order files.

Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.

The code in question was barely three days old by the time it was deprecated anyway.

Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`. We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: timotree3 <timorcb@gmail.com>

) This PR defines an explicit binary product and binary coproduct for functors `F : C ⥤ Type u` for an arbitrary category `C`. This is a generalization of #9704. Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

Interaction of the composition-product of kernels with addition.

…stead of Field (#11232) I need $K$ to be a skew field instead of a field to prove that projectivization of a vector space is a projective geometry stated in proposition 2.1.6 in the book "Modern Projective Geometry" by Claude-Alain Faure and Alfred Frölicher, see p. 27-28. In p.27, just before the proposition, it is noted that "... $K$ is allowed to be a skew field (often called *division ring*)."

Removes `to_additive` from a `MulZeroClass` instance and instead puts it on the corresponding `MulOneClass` instance (more explanation here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20on.20MulZeroClass).

1. `ContinuousAt.comp₂`, `ContinuousAt.comp₂_continuousWithinAt`, and `_of_eq` versions. 2. `ContinuousAt.along_{fst,snd}`: Continuous functions are continuous in their first and second arguments.

)

The squeezing continues! All found by the linter at #11246.

- Add `closure_smul₀'`, a version of `closure_smul₀` assuming `c ≠ 0` and no `T1Space`. - Generalize some lemmas from TVS to a continuous `MulActionWithZero`.

We had duplicated API between topological spaces and uniform spaces. In this PR I mostly deduplicate it with some exceptions: - `SeparationQuotient.lift'` and `SeparationQuotient.map` are leftovers from the old version that are designed to work with uniform spaces; - probably, some theorems/instances still assume `UniformSpace` when `TopologicalSpace` would work. Outside of `UniformSpace/Separation`, I mostly changed `SeparatedSpace` to `T0Space` and `separationRel` to `Inseparable`. I also rewrote a few proofs that were broken by the API change. Fixes #2031

Co-authored-by: Johan Commelin <johan@commelin.net>

This just introduces `L` as a short notation for `LSeries` and `↗f` as notation for `fun n : ℕ ↦ (f n : ℂ)`, both scoped to `LSeries.notation`. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function `N → R`, where `ℕ` coerces to `N` and `R` coerces to `ℂ`) as arguments to `LSeries` etc. The first is for convenience (and agreement with informal math, where we write "L(f, s)"), and the second one considerably simplifies statements involving Dirichlet characters or arithmetic functions like the von Mangoldt function and their L-series. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.

Move: * `Mathlib/Algebra/Module/DirectLimitAndTensorProduct.lean` to `LinearAlgebra/TensorProduct/DirectLimit.lean` * `Mathlib/LinearAlgebra/TensorProduct` to `Mathlib/LinearAlgebra.TensorProduct.Basic.lean` * `Mathlib/RingTheory/TensorProduct` to `Mathlib/RingTheory/TensorProduct/Basic.lean`. This follows suggestions 1, 2, 3 of https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tensor.20Products.20of.20modules.20and.20rings/near/424605543 Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>

Mathematicians will be unnerved by us evaluating the zeta function at 1 and getting a complex number. Pointed out by Jordan Ellenberg on Twitter.

I see no reason for the omission of `@[to_additive]` on these two `pretransitive_iff_...` lemmas, so add it here. From AperiodicMonotilesLean.

... by moving `variable [DecidableEq ι]` to `section`s.

Fixing mathport breakage. Co-authored-by: Mario Carneiro <di.gama@gmail.com>

…tionMonoid.IsPrime.exists_mem_Prime_of_neq_bot (#11218) We add `UniqueFactorizationMonoid.IsPrime.exists_mem_Prime_of_neq_bot`: if an integral domain is a `UniqueFactorizationMonoid`, then every nonzero prime ideal contains a prime element. We plan to add the other implication (known as Kaplansky's criterion) in a future PR. Co-authored-by: EmilieUthaiwat <102412311+EmilieUthaiwat@users.noreply.github.com> Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>

Generalizes the previous definition and moves it into `LinearAlgebra/BilinearMap`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

We add `Commute.orderOf_mul_pow_eq_lcm`: if two commuting elements `x` and `y` of a monoid have order `n` and `m`, there is an element of order `lcm n m`. The result actually gives an explicit (computable) element, written as the product of a power of `x` and a power of `y`. Co-authored-by: Junyan Xu <[junyanxu.math@gmail.com](mailto:junyanxu.math@gmail.com)>

For as yet un-completely diagnosed reasons, `unitary.star_mul_self_of_mem hu` for `(hu : u ∈ unitary (H →L[𝕜] H))` elaborates slowly thanks to `[1.068378s] ✅ ContinuousLinearMap.comp (ContinuousLinearMap.adjoint u) u =?= star ?a * ?b`. This PR pulls out the statements into `have`'s which speeds up the proofs significantly. #11299 documents the issue for future investigation.

#10861)

Currently doesn't simplify since `interior_Icc` goes the other way. We were using it in PrimeNumberTheoremAnd for things like "point does not lie on boundary of rectangle". Co-authored-by: L Lllvvuu <git@llllvvuu.dev>

With `aesop_cat` as `autoParam` this was taking 20-25s to build one declaration. This explicitly provides fills the argument and significantly speeds up the build. A comment is left about the issue. Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>

…1295) Given two equivalence relations with `r ≤ s`, define an equivalence between a sigma type for the sum of the quotients by `r` on each equivalence class by `s`, and the quotient by `r`. The motivating example is bijecting between orbits of an action by a subgroup: the orbits considered within each orbit of the action by the full group are equivalent to the orbits when the subgroup acts directly on the whole space. This is a generic version for an arbitrary pair of setoids with `r ≤ s`, to be used in defining the version for orbits. Feel free to golf or suggest a better name for the equivalence. From AperiodicMonotilesLean.

…10869) Also golf a proof

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

... as a `@[deprecated] alias` Also add dates to some theorems deprecated in #10816, deprecate `Set.exists_range_iff'`, and use `simp`-normal form in the definition of `ParacompactSpace`.

…11307) The currently definition of `piTensorHomMap₂` results in a large term causing `dsimp` and `simp` to work too hard. This PR breaks up the definition into a function defnition and two lemmas. The result is a 17% speed up.

These are more general than the `insert` versions as they do not assume `DecidableEq`. This also lets some later proofs be golfed.

Main definitions - `pNilradical`: the `p`-nilradical of a ring is an ideal consists of elements `x` such that `x ^ p ^ n = 0` for some `n` (`mem_pNilradical`). It is equal to the nilradical if `p > 1` (`pNilradical_eq_nilradical`), otherwise it is equal to zero (`pNilradical_eq_bot`). - `IsPRadical`: a ring homomorphism `i : K →+* L` of characteristic `p` rings is called `p`-radical, if or any element `x` of `L` there is `n : ℕ` such that `x ^ (p ^ n)` is contained in `K`, and the kernel of `i` is contained in the `p`-nilradical of `K`. A generalization of purely inseparable extension for fields. - `IsPerfectClosure`: a ring homomorphism `i : K →+* L` of characteristic `p` rings makes `L` a perfect closure of `K`, if `L` is perfect, and `i` is `p`-radical. - `PerfectRing.lift`: if a `p`-radical ring homomorphism `K →+* L` is given, `M` is a perfect ring, then any ring homomorphism `K →+* M` can be lifted to `L →+* M`. This is similar to `IsAlgClosed.lift` and `IsSepClosed.lift`. - `PerfectRing.liftEquiv`: `K →+* M` is one-to-one correspondence to `L →+* M`, given by `PerfectRing.lift`. This is a generalization to `PerfectClosure.lift`. - `IsPerfectClosure.equiv`: perfect closures of a ring are isomorphic. Main results - `IsPRadical.trans`: composition of `p`-radical ring homomorphisms is also `p`-radical. - `PerfectClosure.isPerfectClosure`: the absolute perfect closure `PerfectClosure` is a perfect closure. - `IsPRadical.isPurelyInseparable`, `IsPurelyInseparable.isPRadical`: `p`-radical and purely inseparable are equivalent for fields. - `perfectClosure.isPerfectClosure`: the (relative) perfect closure `perfectClosure` is a perfect closure.

…10391) This PR defines the class `Profinite.IsLight` which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a `LightProfinite`, and the underlying profinite space of a `LightProfinite` is light. - [x] depends on: #10390

…y of L-series (#11214) This adds a file `NumberTheory.LSeries.Linearity`, which contains statements on * addition (moved from `NumberTheory.LSeries.Basic`) * negation and * scalar multiplication of L-series, and corresponding statements for `LSeries.term`, `LSeriesHasSum` and `LSeriesSummable`. See [this thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip.

Currently the definition of additive characters (from an additive to a multiplicative monoid) is hidden away in `NumberTheory/LegendreSymbol`. These constructions seem to be getting used more widely, e.g. in Yaël's LeanAPAP project; so this PR carves off the parts of `NumberTheory/LegendreSymbol/AddCharacter` which don't depend on cyclotomic field arithmetic and moves them to `Algebra/Group`.

Backported from #11314.

…d add 2 thms (#11303) * Generalize one assumption from `AddCommGroup` to `AddCommMonoid` at one place (no modification of a proof is needed) * Add two lemmas that compute the range of `LinearMap.rTensor` and `LinearMap.lTensor` * Adjust the names of a few lemmas : `rTensor.surjective` becomes `LinearMap.rTensor_surjective`, etc. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>

Per [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Quantum.20information.20theory/near/426134633)

This establishes uniqueness of the continuous functional calculus for unital algebras. When the scalar ring is `ℝ` or `ℂ`, this follows immediately from Stone-Weierstrass, but for `ℝ≥0`, we need to reuse the result for `ℝ`. This is tricky, as we need to upgrade an `ℝ≥0`-algebra homomorphism (with domain `C((s : Set ℝ≥0), ℝ≥0)`) to a `ℝ`-algebra homomorphism (with domain `C(((↑) '' s : Set ℝ), ℝ)`). This is the reason the `UniqueContinuousFunctionalCalculus` class exists in the first place, as opposed to simply appealing directly to Stone-Weierstrass to prove `StarAlgHom.ext_continuousMap`.

This defines the `quasispectrum` of an element `a : A` where `A` is a non-unital `R`-algebra. When `A` is unital and `R` is a semifield, then `quasispectrum R a = spectrum R a ∪ {0}`. The definition proceeds via *quasiregular* elements, which are also defined herein. The quasispectrum will serve as the domain of the continuous functions appearing in the continuous functional calculus for non-unital algebras.

This is a smaller version of #7020. Before this PR, for limits, we gave instances for small indexing categories, but for colimits, we gave instances for `TypeMax`. This PR changes so that we give instances for small indexing categories in both cases. This is more general and also more uniform. Co-authored-by: Joël Riou <rioujoel@gmail.com>

This is now a `rfl` and in the latest nightly becomes a `synTaut`. We remove it.

…lexes (#10764) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…1236) Replace the uniform bound by an eventual uniform bound along the filter.

Fix a typo.

@fgdorais

This if @fgdorais's patch for leanprover-community/batteries#579. Co-authored-by: F. G. Dorais <fgdorais@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Add one lemma stating that an element is a unit if and only if its image through a ring equivalence is a unit.

…ne polynomials (#10404) - `perfectField_iff_splits_of_natSepDegree_eq_one`: A field is perfect if and only if every separable degree one polynomial splits. - add some criteria of a monic polynomial being separable degree one - add some convenient results of separable degree of a polynomial

The removal of some pointless tactics flagged by #11308.

…11349) Similar to the changes for `ChainComplex.mkAux` we remove the ad-hoc `MkStruct` and replace with it `ShortComplex`.

Some basic missing lemmas about injective function composition. See this Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/injective.20function.20composed.20with.20non.20zero.20function.20ne.20zero) Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Let `κ : kernel α β` and `η : kernel (α × β) γ` be two s-finite kernels and `p` a predicate on `β × γ`. If the set `{ x | p x}` is measurable, then `(∀ᵐ bc ∂(κ ⊗ₖ η) a, p bc) ↔ ∀ᵐ b ∂κ a, ∀ᵐ c ∂η (a, b), p (b, c)`.

…10945) In a countably generated measurable space `α`, we can build a sequence of finer and finer finite measurable partitions of the space such that the measurable space is generated by the union of all partitions. This sequence of partitions (`countablePartition α n`) is defined in `MeasureTheory.MeasurableSpace.CountablyGenerated`. This is a new file in which we put the definition of `CountablyGenerated` (which was previously in MeasurableSpace.Basic). In `Probability.Process.CountablyGenerated`, we build the filtration generated by `countablePartition α n` for all `n : ℕ`, which we call `countableFiltration α`. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

…#11275)

Use it to golf `Vitali.exists_disjoint_covering_ae`

…l` (#10742) This is taken from [my zulip message here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/How.20to.20simplify.20this.20proof.20without.20using.20a.20have.20statement.3F/near/422294189). As an example: ```lean example : 2^10 = eval% 2^10 := by -- goal is `2^10 = 1024` sorry ```

Often cleaning up with `dsimp` before using other tactics can speed up unification checks in a proof. This is one such example speeding up this file by 30% on my machine. Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>

…form/inverse (#10944) Co-authored-by: L Lllvvuu <git@llllvvuu.dev> Co-authored-by: L <git@llllvvuu.dev>

... or reduce its scope (the full removal is not as obvious).

I removed some of the tactics that were not used and are hopefully uncontroversial arising from the linter at #11308. As the commit messages should convey, the removed tactics are, essentially, ``` push_cast norm_cast congr norm_num dsimp funext intro infer_instance ```

This PR fixes a test that failed in the upgrade to v4.8.0. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/MoveAdd)

Adds a lemma

Prove `DiscreteTopology.secondCountableTopology_of_countable` directly, deprecate `DiscreteTopology.secondCountableTopology_of_encodable`.

it triggers rebuilds and can be annoying.

Per the style guidelines, `λ` is disallowed in mathlib. This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon. Notes - In lines I was modifying anyway, I also converted `=>` to `↦`. - Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`. - Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced. <!-- The text above the `

…n`. (#11360) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

this will break once leanprover/lean4#3658 lands, so let's fix this now. Also avoids binding unused variables in `termination_by`.

It started with the one in `Convex/Combination` and spiralled into revisiting all notes with `needs` in them. The `ToLin` changes overlap with #11171.

More tactics that are not used, found using the linter at #11308. The PR consists of tactic removals, whitespace changes and replacing a porting note by an explanation.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…l prime ideals (#11201) Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>

This PR introduces a class for categories with explicit choices of binary products and terminal objects, and introduces the associated (Cartesian) symmetric monoidal instance. The primary use of this class is to be able to define internal algebraic objects in categories with chosen finite products, while retaining good definitional properties of the products in question, primarily as a convenience. We introduce an instance of this new class for the category of types where the binary product is the usual type-theoretic product and the terminal object is `PUnit`. Future work will introduce an instance for other categories, especially the category of affine schemes which should make objects like group schemes more convenient. NOTE: In some sense this reverses the refactor done in leanprover-community/mathlib3#3995 but only in the particular case of binary products and terminal objects. Working with (nonexplicit) (co)limits is still the preferred way to work with (co)limits in abstract categories, and instances of `ChosenFiniteProducts` (and other similar classes which may be introduced in the future) should be carefully considered before they are introduced.

) I just needed the `three` version of these when doing some explicit computations with a cubic polynomial. Obviously there is a limit to how far we should go but I think the proposed values are reasonable.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

More unused tactics flagged by the linter (#11308): these are all the changes in `Archive/Counterexamples` that the linter found.

The termination checker has been getting more capable, and many of the `termination_by` or `decreasing_by` clauses in Mathlib are no longer needed. (Note that `termination_by?` will show the automatically derived termination expression, so no information is being lost by removing these.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…image_convexHull` (#11298) - flip `LinearMap.convexHull_image` and rename to `image_convexHull` - while at it, also flip the direction of `convexHull_smul` and `convexHull_neg` to match this - fix argument order of `AffineMap.convexHull_image`: have the `AffineMap` argument come first; there's no good reason not to and this enables dot notation - inline variable `(s : Set E)` to achieve this; this is slightly clearer anyway [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/image_convexHull.20vs.20convexHull_image)

Also add two missing `simp` attributes

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

It doesn't make a lot of sense for `factors` to require a `DecidableEq` assumption since it's not used in the statement, and the definition is already noncomputable. This PR removes that assumption and updates some lemmas later in the file accordingly.

…ras (#11221)

#10822) Only the other direction exists currently, it seems.

@fpvandoorn

…11157) The general policy in mathlib is to include decidability assumptions on a theorem if and only if they are used in its statement. @fpvandoorn has been working on a linter to detect cases which violate the backwards direction of that policy. (i.e. cases where `Classical.propDecidable` appears in a theorem's statement.) I've started going through [the output of that linter](https://gist.github.com/fpvandoorn/05cca028139e98bded9874169a1332d5) and this PR contains fixes for the two files I've finished so far. [Zulip thread about the linter](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/prop.20decidable.20linter/near/424101789)

… with support bounded below (#9574) Given a locally finite linearly ordered set `Γ` and a function `f` on `Γ` whose support is bounded below, we produce a Hahn series whose coefficients are given by `f`. We introduce a theorem (borrowing from mathlib3 #18604) for translating the vanishing condition to the partially well-ordered support condition that is used in the definition of Hahn Series.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Make `extract_lets` (without any specified `at`) work on just the goal. This supplements the already valid syntax `extract_lets at h ⊢` and `extract_lets at *`

The non-dependent version of `DFunLike.{fintype,finite}` is called `FunLike.{fintype,finite}`; the names in the docstring do not exist.

This new order matches the order in the `extends` clause, and so results in less eta expansion. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Co-authored-by: damiano <adomani@gmail.com>

@ADedecker

* Make it work for a `UniformSpace` with extra properties. * Use it to golf some instances. Co-authored-by: @ADedecker

This PR combines several results involving topological sums over `ℤ`. These results are used in #10011 (Hurwitz zeta functions) where sums over `ℤ` feature heavily. * Fill in `tsum` and `Summable` variants for lemmas proved for `HasSum` * Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme * Generalise several lemmas to allow the target space to be a topological monoid rather than a group. * Speed up some slow proofs (the old `summable_int_of_summable_nat` took about 10s to compile on my machine, its replacement `Summable.of_nat_of_neg` is 1000 times faster)

This PR removes the `simps` attribute in the definition of the category structure on `SimplexCategory` so as to prevent API leakage. Better suited `simp` lemmas are added. The definition of `SimplexCategory.const` is also generalized in order to describe any constant map in `SimplexCategory`.

…le (#11403) - Remove Lean 3 syntax in comments: there's no reason it should be there. - Indent the 'by' blocks according to the style guide. - Add some blank lines at beginnings of sections; that's good practice.

Two comments with Lean 3 code looked like they should have been labelled "porting note". Do so; one of them can be fixed now.

…me constructions (#10732) The main addition is `IsTopologicalBasis.inf` (see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Inf.20of.20a.20pair.20of.20topologies/near/419989448), and I also reordered things to be in the more typical order (deducing the `Pi` version from the `iInf` version rather than the converse). Also a few extra golfs and variations. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>

From sphere-eversion; I adapted the proof to mathlib's definition and golfed it a bit. This adds a new import; as this file is not imported anywhere, this seems fine.

Classifies by adding issue number #11036 to porting notes claiming: > dot notation no longer works

* Assume `[Finite J]` instead of `[Fintype J]` whenever we don't need data to formulate the theorem. * Drop `[DecidableEq]` assumptions in `biproduct.reindex`.

This PR proposes two changes to CI. ### Quiet `Archive` and `Counterexamples` CI checks that building `Mathlib` and `test` produces no messages. However, `Archive` and `Counterexamples` could be noisy and CI would not detect it. This PR makes sure that also `Archive and `Counterexamples` are quiet. I noticed that `Archive` and `Counterexamples` were not required to be quiet, since they contained unused tactics flagged by the linter. EDIT: this second item is already available -- see Floris' comment below. ### Upload the cache even when `Mathlib` is noisy This PR moves the check of quietness of `Mathlib` until after the uploading cache step, so that you can have the cache available to fix the noisiness! As a check, PR #11378 made `Mathlib` noisy, CI failed, but only after uploading the cache and building `Archive`, `Counterexamples`. See in particular [this CI run](https://github.com/leanprover-community/mathlib4/actions/runs/8285030855/job/22671860704).

Following discussion at #11313 this is an attempt to refactor `Algebra/Group/AddChar.lean` such that `AddChar A M` is a structure in its own right rather than a type synonym for `Multiplicative A →* M`. We also relax typeclass assumptions considerably (only assuming commutativity, etc, where it is really needed) and add some new functionality, e.g. composition with monoid morphisms on either side (`MonoidHom.compAddChar` and `AddChar.compAddMonoidHom`).

Currently `Equiv.algebra` is defined in terms of `RingHom.toAlgebra'` which causes the induced `Module R` instance to not be defeq to the one from `Equiv.module`. This commit fixes this by defining `Equiv.algebra` in terms of `Algebra.ofModule`.

Includes some doc comments and real code: this is exhaustive, with two exceptions: - some files are handled in #11409 instead - I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std. Follow-up to #11301, much shorter this time.

It's deprecated in favour of `variable`; likely a leftover from the port. Also replace `universes`, which is invalid now.

Double-checking the syntax is welcome.

Best reviewed commit by commit.

…on (#10406) This PR establishes an easy topology comparison: the topology given by the Lévy-Prokhorov distance is finer than the topology of convergence in distribution. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com> Co-authored-by: kkytola <“kalle.kytola@aalto.fi”> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Resolves porting notes claiming "`apply` → `induction`" since the new `induction` is more idiomatic than `apply`.

Let `κ : kernel α (β × ℝ)` and `ν : kernel α β` be two finite kernels. A function `f : α × β → StieltjesFunction` is called a conditional kernel CDF of `κ` with respect to `ν` if it is measurable, tends to to 0 at -∞ and to 1 at +∞ for all `p : α × β`, if `fun b ↦ f (a, b) x` is `(ν a)`-integrable for all `a : α` and `x : ℝ` and for all measurable sets `s : Set β`, `∫ b in s, f (a, b) x ∂(ν a) = (κ a (s ×ˢ Iic x)).toReal`. From such a function with property `hf : IsCondKernelCDF f κ ν`, we build a `kernel (α × β) ℝ` denoted by `hf.toKernel f` such that `κ = ν ⊗ₖ hf.toKernel f`. The new file has substantial overlap with the contents of `Probability.Kernel.Disintegration` and `Probability.Kernel.CondCdf`: these two files will later be refactored to use the code in this PR. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

These are the case names used by the `induction` tactic after the `with`. This replaces `H0`, `H1`, `Hmul` etc with `zero`, `one`, `mul`. This PR does not touch `Submonoid` or `Subgroup`, as `to_additive` does not know how to rename the argument names. There are ways to work around this, but I'd prefer to leave them to a later PR. This also leaves the `closure_induction₂` variants alone, as renaming the arguments is more work for less gain.

Move `factors_zero` up, use it to golf `ne_zero_of_mem_factors`

Use `classical` instead

Classifies by adding issue number #10756 to porting notes claiming anything equivalent to: - "added theorem" - "added theorems" - "new theorem" - "new theorems" - "added lemma" - "new lemma" - "new lemmas"

Classifies by adding issue number #10754 to porting notes claiming "new instance".

Classifies by adding issue number #11441 to porting notes claiming: > `rfl` required.

Classifies by adding issue number #11445 to porting notes claiming anything equivalent to: - "new definition" - "added definition"

Classifies by adding issue number #11180 to porting notes claiming: > removed `@[pp_nodot]`

This PR changes the behaviour of CI: after an unsuccessful `shake`, CI will continue to lint mathlib. You can take a look at #11452 for an example of the CI proposed in this PR acting in a situation where an unused import is present. `shake` fails, but CI still linted mathlib. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/CI.3A.20continue.20on.20failure.3F/near/426905828)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

We define the group homomorphism Aut(L)->(Z/dZ)^* coming from the action on the n'th roots of unity in L. Here d is the number of n'th roots of unity in L (which might not be n in this generality). We also make API for the standard special case when there are n n'th roots of unity in L, calling it `ModularCyclotomicCharacter`. Joint work with Hanneke Wiersema, coming from the Leiden conference on machine checked mathematics.

Classifies by adding issue number #10618 to porting notes claiming > `@[simp]` can prove

…11371) It's about `LocallyFiniteOrderBot`, so the current name is simply wrong. Also fix documentation mistakes. These errors were already present in Mathlib 3, before the port. Co-authored-by: Richard Copley <rcopley@gmail.com>

Also, in some cases drop unneeded `Fintype` arguments.

See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)

Empty lines were removed by executing the following Python script twice ```python import os import re # Loop through each file in the repository for dir_path, dirs, files in os.walk('.'): for filename in files: if filename.endswith('.lean'): file_path = os.path.join(dir_path, filename) # Open the file and read its contents with open(file_path, 'r') as file: content = file.read() # Use a regular expression to replace sequences of "variable" lines separated by empty lines # with sequences without empty lines modified_content = re.sub(r'(variable.*\n)\n(variable(?! .* in))', r'\1\2', content) # Write the modified content back to the file with open(file_path, 'w') as file: file.write(modified_content) ```

@samvang

Remove the assumption that the type be a distributive lattice when partial order suffices in Birkhoff's representation theorem. Co-authored by : Sam van Gool @samvang Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Sam <59202064+samvang@users.noreply.github.com> Co-authored-by: samvang <59202064+samvang@users.noreply.github.com>

… of bifunctors (#10747) When bifunctors `F₁₂`, `G`, `F` and `G₂₃` are equipped with a natural isomorphism `G(F₁₂(X₁, X₂), X₃) ≅ F(X₁, G₂₃(X₂, X₃))` in three variables, then under reasonable assumptions and conditions on indices, there is an associator isomorphism for the action of these bifunctors on graded objects `mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ ≅mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)`. This shall be used in order to construct the associator isomorphism for the monoidal category structure on graded objects. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…argument (#11056) Given a family of morphisms `f i : A i ⟶ B i` in a category `C` and an object `S : C`, we define a functor `SmallObject.functor f S : Over S ⥤ Over S` which shall play an important role in the formalization of the "small object argument". Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

@Vierkantor

…dules over commutative semirings (#11280) Require the module in the definition of the `BilinForm` structure to be over a commutative semiring. This PR is a per-requisite for #11278. It supersedes #10422. It's been pointed out elsewhere that the current definition over a non-commutative semiring doesn't make mathematical sense: #10553 (comment) Eventually the non-commutative situation may be considered in a mathematically meaningful way in the context of sesquilinear maps (e.g. something like #9334 (review)). Co-authored-by: @Vierkantor Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…1463) Add two more lemmas about orbits in a `SubMulAction`, both closely related to the existing `val_image_orbit`. From AperiodicMonotilesLean. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Previously this file was read four times at runtime, and once for each file at compile time. Now it is read only once, when `lake exe cache` is run. `initialize` is not a substitute for correctly passing global state through a program; my impression is that it is intended for *language-* rather than program-level initialization. The performance impact is negligible, but the new code is more predictable. Tested on mathlib, and on a package created using `lake new foo math`, pointed at this mathlib branch. `lake exe cache get` works correctly (leaves `lake build` with nothing to do) in both cases.

Co-authored-by: adomani <adomani@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

After #11148, all results about concrete limits and colimits hold whenever the relevant (co)limits exist, which is optimal. Thanks to Joël Riou for making this possible!

…0923) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Use `Nat` specialized theorems, and `omega`, where necessary to avoid needing to import the abstract ordered algebra hierarchy for basic results about `List`. Import graph between `Mathlib.Order.Basic` and `Mathlib.Data.List.Basic`: * [before.pdf](https://github.com/leanprover-community/mathlib4/files/14646805/before.pdf) * [after.pdf](https://github.com/leanprover-community/mathlib4/files/14646804/after.pdf) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…o the shifts (#10854) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Hopefully has no effect except to remove some warnings in the build logs. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…Epimorphic/Basic.lean` (#11458) Adds no new material, just splits the file into smaller chunks and removes a couple of useless lemmas. - [x] depends on: #11457

For a `ℤ`-lattice `L` of `E`, defined as a discrete subgroup that spans the whole space `E` over `K`, proves that any `ℤ`-basis of `L` is also a `K`-basis of `E`. This provides the link between the two points of view on lattices in this file.

Move from `Algebra.GroupWithZero.Units.Lemmas` to `Algebra.GroupWithZero.Units.Basic` the lemmas that can be moved.

as it conflicts with `xor_comm` in the root namespace. Also protect `Nat.xor_assoc` in case someone adds `xor_assoc`.

This renames the arguments to the eliminators to be more ergonomic when using the `induction` tactic. I also changed the definition in an attempt to make the proof easier.

Adds the following missing theorem ``` theorem mulVec_sub [Fintype n] (A : Matrix m n α) (x y : n → α) : A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y ``` Currently there only is ```mulVec_sub```. I asked about it here on [zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/No.20theorem.20Matrix.2EmulVec_sub).

…nge (#11438) All these lemmas refer to the range of some function being open/range (i.e. `isOpen` or `isClosed`).

#11505) We define `TensorProduct.addCommMonoid` in terms of `TensorProduct.addMonoid` to reduce unfolding.

Classifies by adding issue number #11446 to porting notes claiming "added definition".

Classifies by adding issue number #11432 to porting notes claiming "added theorem" or "added lemma".

These lemmas can be defined earlier, ridding us of an import in `Algebra.GroupPower.Order`

From #9267 (comment): > I would prefer we use lattice operations for adding edges. The idea is to make constructor `SimpleGraph.edge (v w : V) : SimpleGraph V` that creates a graph with a single edge between `v` and `w` if they're not equal (and no edge if they are), and then `G.addEdge v w` would instead be `G ⊔ edge v w`. This is more versatile, though perhaps lemmas such as `addEdge_of_adj` are a bit more brittle to apply.

Generalize `coclosedCompact_eq_cocompact` and `relativelyCompact`.

@kmill

Co-authored-by: @kmill , @thorimur Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

These lemmas are needed to define the semifield structure on `NNRat`, hence I am repurposing `Algebra.Order.Field.Defs` from avoiding a timeout (which I believe was solved long ago) to avoiding to import random stuff in the definition of the semifield structure on `NNRat` (although this PR doesn't actually reduce imports there, it will be in a later PR). Reduce the diff of #11203

All the unnamed instances here were very long, and Moritz recently linked one of these to a newcomer. Also slightly clean up the `Lattice` instance

This is presumably not exhaustive, but covers about a hundred instances. Style opinions (e.g., why a particular change is great/not a good idea) are very welcome; I'm still forming my own.

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

... and add a deprecated alias for the old name. This is mostly just me discovering the power of `F2`

- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.

@loefflerd

Sometimes, that line can be golfed into the next line. Inspired by a [comment](#11208 (comment)) of @loefflerd; any decisions are my own.

- replace apply foo.mpr by rw [foo], golfing into the next line - replace a few `@foo _ _ _` by named arguments

Fixes breakage from #11507.

Let `κ : kernel α (γ × β)` and `ν : kernel α γ` be two finite kernels with `kernel.fst κ ≤ ν`, where `γ` has a countably generated σ-algebra (true in particular for standard Borel spaces). We build a function `f : α → γ → Set β → ℝ` jointly measurable in the first two arguments such that for all `a : α` and all measurable sets `s : Set β` and `A : Set γ`, `∫ x in A, f a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal`. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

A general framework for proving analytic continuation & functional equations via Mellin transforms.

This adds a file `Mathlib.NumberTheory.LSeries.Deriv` that contains results on differentiability and derivatives of L-series, including the fact that the L-series is holomorphic on its right half-plane of absolute convergence. See [this thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/424858837) on Zulip. Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

Makes the proof of this lemma shorter and perhaps cleaner by adding a new lemma and moving it forward to take advantage of the preexisting `card_eq_three` Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

…tCast` (#11552) Reduce the diff of #11499

Some small changes to adapt to the 2024-03-16 nightly that can land in advance.

#11493) - Add `FreeGroup.closure_range_of`: the subgroup closure of the range of `FreeGroup.of : α → FreeGroup α` is `⊤`. (That is, the generators of a free group generate the free group.) - Add `PresentedGroup.closure_range_of`: the subgroup closure of the range of `PresentedGroup.of : α → PresentedGroup rels` is `⊤`. (That is, the generators of a presented group generate the presented group.)

Removes the `insertNth` section of this long file to its own new file. This section seems to be completely independent of the rest of the file, so this is a fairly easy split to make.

Classifies by adding issue number #10618 to porting notes claiming "`simp` can prove it".

This will become an error in 2024-03-16 nightly, possibly not permanently. Co-authored-by: Scott Morrison <scott@tqft.net>

…asic lemmas (#11561) Move lemmas to put similar ones together, replace `refine'` by `refine` and `=>` by `↦`. Lemmas added: * `singularPart_add_rnDeriv` and `rnDeriv_add_singularPart`: almost aliases of `haveLebesgueDecomposition_add` * `haveLebesgueDecomposition_smul'`, `haveLebesgueDecomposition_rnDeriv` * `singularPart_eq_zero_of_ac`, `singularPart_eq_zero`, `singularPart_self`, `singularPart_eq_self` Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Summability of `n ↦ 1 / |n + a| ^ s` and `n ↦ n ^ k exp (-r * n)`

…11373)

.. in `equivOfPiLEquivPi`, `coePiBasisFun.toMatrix_eq_transpose`, `vecMul_surjective_iff_exists_left_inverse`, and `mulVec_surjective_iff_exists_right_inverse`

Also rename `*lpBcf` to `*lpBCF` and drop 2 duplicate instances.

Adds a congruence lemma for `BEq` instances that makes use of `LawfulBEq` instances, and gives `congr!` the ability to use this congruence lemma. This is meant to help with diamonds that arise from interactions between Decidable and BEq instances. This feature can be turned off using the `beqEq` configuration setting, like `congr! (config := { beqEq := false })`.

Currently you need to run ``` lake build ProofWidgets make tests ``` to reliably get tests to work. ---  [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Condensed): light condensed objects #9515

feat(Condensed): light condensed objects #9515

Commits on Mar 22, 2024