[Merged by Bors] - feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal #21900

Thmoas-Guan · 2025-02-15T07:34:43Z

Define transtition map between ring or module quotient by powers of ideal, both for developing API for IsAdicComplete

Co-authored-by: @jjdishere [email protected]

github-actions · 2025-02-15T07:35:37Z

PR summary 7ef91e6a7f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
53 files `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.NumberTheory.Padics.MahlerBasis` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.ZetaValues` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.AdicCompletion.Exactness` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.RingTheory.AdicCompletion.Noetherian` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Henselian` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.Perfectoid.Untilt` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.RingTheory.WittVector.Complete` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.Topology.Algebra.Valued.LocallyCompact`	1
`Mathlib.RingTheory.Ideal.Quotient.PowTransition` (new file)	1057

Declarations diff

+ Ideal.Quotient.factor_ker
+ factor
+ factor_comp_mk
+ factor_eq
+ factor_mk
+ mapQ_eq_factor
+ pow_smul_top_le
++ factorPow
++ factorPowSucc
++ factor_comp
++ factor_comp_apply
++ factor_surjective
- transitionMap_comp
- transitionMap_comp_apply
- transitionMap_eq
- transitionMap_mk

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

riccardobrasca

I've nothing against this, but I am worried that people start proving stuff about your map instead of the more general factor. Can you explain a little why you think this is really needed? Instead of, for example, working with an abbrev or something.

Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean

Thmoas-Guan · 2025-02-15T11:00:45Z

I've nothing against this, but I am worried that people start proving stuff about your map instead of the more general factor. Can you explain a little why you think this is really needed? Instead of, for example, working with an abbrev or something.

For me I doesn't need it that urgently, the only cost of using the module version is a bit longer and more ugly proof. The real reason may need @jjdishere to answer.
Also there is an problem remaining: the version of mapQPow he proposed is only the special case for AdicCompletion.transitionMap for adjcent integer and the current version is the exact same, we may need some more discussion.

Thmoas-Guan · 2025-02-15T11:31:05Z

The result of the discussion is we decide to separate AdicCompletion.transitionMap out of AdicCompletion.Basic to this file, and leave the AdicCompletion.transitionMap and the ones for adjcent onns as abbreviations. What do you think?

and abbrev for succ

erdOne

I think all these lemmas are about Ideal.factor and not specific to this.
Can you please add the missing lemmas to Ideal.factor so that all lemmas about factorPow are one-lemma term proofs? And then I would hope we don't need this anymore.

For the module side maybe an analogous Submodule.factor could be added? But it looks like every thing should work for general mapQ. OTOH I ^ n • ⊤ <= I ^ m • ⊤ might be a nice lemma to have.

erdOne · 2025-02-16T10:48:54Z

Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean

+abbrev mapQPow {m n : ℕ} (le : m ≤ n) :
+    M ⧸ (I ^ n • ⊤ : Submodule R M) →ₗ[R] M ⧸ (I ^ m • ⊤ : Submodule R M) :=
+  liftQ (I ^ n • ⊤ : Submodule R M) (mkQ (I ^ m • ⊤ : Submodule R M))
+    ((ker_mkQ (I ^ m • ⊤ : Submodule R M)).symm ▸ (smul_mono_left (pow_le_pow_right le)))


We should use Submodule.mapQ here.

Although I only copied this from AdicCompletion.TransitionMap , I have only one small question : what is the advantage of mapQ?

It gets rid of (ker_mkQ (I ^ m • ⊤ : Submodule R M)).symm ▸ and has the possibility of a more tailored api.

I think the ▸ can't be get rid of, like this

mapQ _ _ LinearMap.id (comap_id (I ^ n • ⊤ : Submodule R M) ▸ smul_mono_left (pow_le_pow_right n.le_succ))

comap_id is refl though. Does it not work if you remove it?

sorry, it worked, my fault.

I have anothor small question here, why Ideal.Quotient.factor need the two Ideals to be explicit? The le condition already gave the two? So in Submodule.factor how should I set the variables?

There two possibilities:

it is just a mistake

it helps Lean with unification

You can try to modify Ideal.Quotient.factor and see if you need (I := ...) somewhere. If not I am happy to change to implicit variables.

I've opened #22022, I think we don't need (I := ...) anywhere.
However Quot.factor have these two variable explicit, I don't know if we need to unify.

Thmoas-Guan · 2025-02-16T12:22:10Z

I think all these lemmas are about Ideal.factor and not specific to this. Can you please add the missing lemmas to Ideal.factor so that all lemmas about factorPow are one-lemma term proofs? And then I would hope we don't need this anymore.

For the module side maybe an analogous Submodule.factor could be added? But it looks like every thing should work for general mapQ. OTOH I ^ n • ⊤ <= I ^ m • ⊤ might be a nice lemma to have.

I agree that most of these simp lemmas are only the missing things in Ideal.factor. However I think that Submodule.factor should exist. After this we can wrap the special case AdicCompletion.TransitionMap and AdicCompletion.TransitionMapSucc along with the corresponding ring version into abbrev, what is your opinion @jjdishere ?

jjdishere · 2025-02-17T14:03:51Z

I think all these lemmas are about Ideal.factor and not specific to this. Can you please add the missing lemmas to Ideal.factor so that all lemmas about factorPow are one-lemma term proofs? And then I would hope we don't need this anymore.
For the module side maybe an analogous Submodule.factor could be added? But it looks like every thing should work for general mapQ. OTOH I ^ n • ⊤ <= I ^ m • ⊤ might be a nice lemma to have.

I agree that most of these simp lemmas are only the missing things in Ideal.factor. However I think that Submodule.factor should exist. After this we can wrap the special case AdicCompletion.TransitionMap and AdicCompletion.TransitionMapSucc along with the corresponding ring version into abbrev, what is your opinion @jjdishere ?

I agree. And I also support the idea of "one-lemma term proofs". Without suitable lemmas, these holes need several terms combined with ▸ to solve. If we allow these to be separate lemmas, life is much easier.

This reverts commit c355b1a.

This reverts commit aa42b3a.

This reverts commit f4e4e7b.

Mathlib/LinearAlgebra/Quotient/Basic.lean

Mathlib/RingTheory/Ideal/Quotient/Defs.lean

Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean

riccardobrasca · 2025-02-20T15:15:20Z

LGTM, thanks. One last thing: can you a comment around factor (maybe in the docstring) explaining that in the very common case of M^n and M^m there is a dedicated API? Thanks!

bors d+

mathlib-bors · 2025-02-20T15:15:24Z

✌️ Thmoas-Guan can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

and fix naming

Thmoas-Guan · 2025-02-20T15:53:03Z

dedicated

There are some name fix, can you have another look @riccardobrasca ? Thanks.

riccardobrasca · 2025-02-20T16:03:12Z

LGTM, thanks!

Thmoas-Guan · 2025-02-20T16:20:11Z

bors r+

@jjdishere

…or module quotient by powers of ideal (#21900) Define transtition map between ring or module quotient by powers of ideal, both for developing API for IsAdicComplete Co-authored-by: @jjdishere [email protected] Co-authored-by: jjdishere <[email protected]>

mathlib-bors · 2025-02-20T18:07:27Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (823 commits) chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) feat: `Fintype Ordering` (#22154) chore: more renamings to fit the naming convention (#22148) feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) chore: rename `{Continuous., continuous_}sum_map` to `sumMap` (#22155) chore: remove initial space followed by `-/` (#22158) chore: make arg in HeightOneSpectrum.valuation explicit (#22139) feat(Data/List): `List.maximum` is monotone (#22091) chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] (#21123) chore: backport changes to `getElem` lemmas (#22146) feat(CategoryTheory): generating monomorphisms in Grothendieck abelian categories (#22150) feat: rename variables to fit doc (#22143) feat(CategoryTheory): IsDetecting.isIso_iff_of_mono (#22135) feat(CategoryTheory): truncations of transfinite compositions (#22149) chore: simplify a proof (#22134) feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories (#22133) feat(Order): Set.Ici.isSuccLimit_coe (#22103) chore(Analysis/Convex/Normed): split into smaller files (#22015) feat(Algebra/Algebra/Lie): max nilpotent ideal <= radical (#22140) refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130) chore: rename Injective.sum_elim and friends (#22129) chore: fix naming oversight from #22070 (#22128) chore: fix spelling mistakes (#22136) feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) fix: initialize_simps_projections print warning when projection data already exists (#20339) chore: rename ContMDiff.sum_{elim,map} (#22131) feat(CategoryTheory): characterization of injective objects in terms of lifting properties (#22104) chore(Lean,Tactic): un-indent some doc-strings (#22118) feat(Algebra/MvPolynomial): add `comp` versions of rename lemmas (#21259) chose: add deprecation (#22124) feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) feat(CategoryTheory/Subobject): hasCardinalLT_of_mono (#22122) feat: add `DenseRange.piMap` (#22114) feat(Algebra/Algebra/Lie): define the maximal nilpotent ideal of Lie algebras (#22061) chore(Data/Finset): don't import algebra when defining `Finset.card` (#21866) feat: a function on a discrete space is smooth (#22113) feat: commutative group objects in additive categories (#21521) style(Geometry/Manifold): remove superfluous indentation in doc-strings (#22117) chore: rename PushNeg.lean to Push.lean (#22108) feat: add Is{Open,Closed}Embedding.sum_elim (#22070) feat(RingTheory/Perfectoid): define the untilt map and generalize pretilt (#21563) feature(Topology/Algebra/Module/WeakBilin): Linear map from F into the topological dual of E with the weak topology (#21078) feat(CategoryTheory/Abelian): the exact sequence attached to a pushout square (#22110) chore(ChartedSpace.lean): group constructions together (#22107) feat(CategoryTheory/MorphismProperty): more basic API (#22099) chore(Data/Fintype): split `Fintype/Card.lean` (#21840) chore(SetTheory/Cardinal/Cofinality): make `IsStrongLimit` into a structure (#21971) feat(Combinatorics/SimpleGraph): Add a theorem about cliques in induced subgraphs (#20705) ...

@pechersky

* polynomial-sequences: (558 commits) Correct the TODO to mention IsCancelAdd which does exist. Talk about strict monotonicity instead, thanks @pechersky. Mention the TODO on li generalization to semirings. One more dedent. Same injectivity twiddling for basis. nontiviality to simplify this proof, and some dedenting. Hopefully more correct injectivity lemmas matching the naming convention. Fix the empty docstring. Update Mathlib/Algebra/Polynomial/Sequence.lean Fix the variable naming. Apply suggestions from code review chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) feat: `Fintype Ordering` (#22154) chore: more renamings to fit the naming convention (#22148) feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) chore: rename `{Continuous., continuous_}sum_map` to `sumMap` (#22155) chore: remove initial space followed by `-/` (#22158) chore: make arg in HeightOneSpectrum.valuation explicit (#22139) feat(Data/List): `List.maximum` is monotone (#22091) chore(Combinatorics/SimpleGraph): extract WalkDecomp from Walk (#21981) feat: if a monoid M acts, then so does (s : S) with [SubmonoidClass S M] (#21123) chore: backport changes to `getElem` lemmas (#22146) feat(CategoryTheory): generating monomorphisms in Grothendieck abelian categories (#22150) feat: rename variables to fit doc (#22143) feat(CategoryTheory): IsDetecting.isIso_iff_of_mono (#22135) feat(CategoryTheory): truncations of transfinite compositions (#22149) chore: simplify a proof (#22134) feat(CategoryTheory): monomorphisms are stable under coproducts in Grothendieck abelian categories (#22133) feat(Order): Set.Ici.isSuccLimit_coe (#22103) chore(Analysis/Convex/Normed): split into smaller files (#22015) feat(Algebra/Algebra/Lie): max nilpotent ideal <= radical (#22140) refactor(LinearIndependent): refactor to use LinearIndepOn (#21886) chore: rename some more `Foo.sum_elim` -> `sumElim` (#22130) chore: rename Injective.sum_elim and friends (#22129) chore: fix naming oversight from #22070 (#22128) chore: fix spelling mistakes (#22136) feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal (#21900) fix: initialize_simps_projections print warning when projection data already exists (#20339) chore: rename ContMDiff.sum_{elim,map} (#22131) feat(CategoryTheory): characterization of injective objects in terms of lifting properties (#22104) chore(Lean,Tactic): un-indent some doc-strings (#22118) feat(Algebra/MvPolynomial): add `comp` versions of rename lemmas (#21259) chose: add deprecation (#22124) feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) feat(CategoryTheory/Subobject): hasCardinalLT_of_mono (#22122) feat: add `DenseRange.piMap` (#22114) feat(Algebra/Algebra/Lie): define the maximal nilpotent ideal of Lie algebras (#22061) chore(Data/Finset): don't import algebra when defining `Finset.card` (#21866) feat: a function on a discrete space is smooth (#22113) feat: commutative group objects in additive categories (#21521) ...

define transtition map between quotient powers

10b2fb6

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Feb 15, 2025

Thmoas-Guan added 3 commits February 15, 2025 16:07

Update Mathlib.lean

989392e

add lemma about kernel

0f299f9

fix file name and docstring

23cfc96

Thmoas-Guan mentioned this pull request Feb 15, 2025

feat(RingTheory/Powerseries): Weierstrass preparation #21859

Open

2 tasks

riccardobrasca reviewed Feb 15, 2025

View reviewed changes

Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean Outdated Show resolved Hide resolved

move head doc

789ec58

Thmoas-Guan added 5 commits February 15, 2025 20:53

move AdicCompletion.transitionMap and its simp lemmas

be9a1c8

and abbrev for succ

fix for moved lemma

4cd4aa3

change def into abbrev

b996860

add docstring

73909e0

fix mistake

4fcd60e

Thmoas-Guan mentioned this pull request Feb 16, 2025

feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring #21944

Open

1 task

erdOne reviewed Feb 16, 2025

View reviewed changes

Thmoas-Guan added 3 commits February 17, 2025 20:08

move lemma to appropriate condition

75754a9

fix proof

40643af

fix proof

c355b1a

Thmoas-Guan added 7 commits February 17, 2025 22:11

restore simp lemma

f4e4e7b

Revert "fix proof"

aa42b3a

This reverts commit c355b1a.

Reapply "fix proof"

c0de212

This reverts commit aa42b3a.

Revert "restore simp lemma"

3345f1b

This reverts commit f4e4e7b.

remove useless lemma

b6e7b08

fix def

9ae2e5f

fix linter

f0bbf06

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2025

Merge branch 'master' into transition-map-for-adic-complete-ring

a0fe348

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2025

make variable implicit in Submodule.factor

8880d49

jjdishere mentioned this pull request Feb 20, 2025

feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete #21582

Open

jjdishere requested a review from riccardobrasca February 20, 2025 09:20

riccardobrasca reviewed Feb 20, 2025

View reviewed changes

Mathlib/LinearAlgebra/Quotient/Basic.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Ideal/Quotient/Defs.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean Show resolved Hide resolved

jjdishere added 2 commits February 20, 2025 22:24

fix

8e952bc

add one more lemma

5d5b757

jjdishere added the awaiting-CI label Feb 20, 2025

jjdishere requested a review from riccardobrasca February 20, 2025 14:31

github-actions bot removed the awaiting-CI label Feb 20, 2025

leanprover-community-mathlib4-bot added the delegated label Feb 20, 2025

add doc refer factorPow

7ef91e6

and fix naming

mathlib-bors bot changed the title ~~feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal~~ [Merged by Bors] - feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal Feb 20, 2025

mathlib-bors bot closed this Feb 20, 2025

mathlib-bors bot deleted the transition-map-for-adic-complete-ring branch February 20, 2025 18:07

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal #21900

[Merged by Bors] - feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal #21900

Thmoas-Guan commented Feb 15, 2025

github-actions bot commented Feb 15, 2025 •

edited

Loading

Declarations diff

riccardobrasca left a comment

Thmoas-Guan commented Feb 15, 2025

Thmoas-Guan commented Feb 15, 2025

erdOne left a comment

erdOne Feb 16, 2025

Thmoas-Guan Feb 16, 2025 •

edited

Loading

erdOne Feb 16, 2025

Thmoas-Guan Feb 17, 2025 •

edited

Loading

erdOne Feb 17, 2025

Thmoas-Guan Feb 17, 2025

Thmoas-Guan Feb 17, 2025 •

edited

Loading

riccardobrasca Feb 17, 2025

Thmoas-Guan Feb 17, 2025 •

edited

Loading

Thmoas-Guan commented Feb 16, 2025 •

edited

Loading

jjdishere commented Feb 17, 2025

riccardobrasca commented Feb 20, 2025

mathlib-bors bot commented Feb 20, 2025

Thmoas-Guan commented Feb 20, 2025 •

edited

Loading

riccardobrasca commented Feb 20, 2025

Thmoas-Guan commented Feb 20, 2025

mathlib-bors bot commented Feb 20, 2025

[Merged by Bors] - feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal #21900

[Merged by Bors] - feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal #21900

Conversation

Thmoas-Guan commented Feb 15, 2025

github-actions bot commented Feb 15, 2025 • edited Loading

PR summary 7ef91e6a7f

Import changes for modified files

Declarations diff

riccardobrasca left a comment

Choose a reason for hiding this comment

Thmoas-Guan commented Feb 15, 2025

Thmoas-Guan commented Feb 15, 2025

erdOne left a comment

Choose a reason for hiding this comment

erdOne Feb 16, 2025

Choose a reason for hiding this comment

Thmoas-Guan Feb 16, 2025 • edited Loading

Choose a reason for hiding this comment

erdOne Feb 16, 2025

Choose a reason for hiding this comment

Thmoas-Guan Feb 17, 2025 • edited Loading

Choose a reason for hiding this comment

erdOne Feb 17, 2025

Choose a reason for hiding this comment

Thmoas-Guan Feb 17, 2025

Choose a reason for hiding this comment

Thmoas-Guan Feb 17, 2025 • edited Loading

Choose a reason for hiding this comment

riccardobrasca Feb 17, 2025

Choose a reason for hiding this comment

Thmoas-Guan Feb 17, 2025 • edited Loading

Choose a reason for hiding this comment

Thmoas-Guan commented Feb 16, 2025 • edited Loading

jjdishere commented Feb 17, 2025

riccardobrasca commented Feb 20, 2025

mathlib-bors bot commented Feb 20, 2025

Thmoas-Guan commented Feb 20, 2025 • edited Loading

riccardobrasca commented Feb 20, 2025

Thmoas-Guan commented Feb 20, 2025

mathlib-bors bot commented Feb 20, 2025

github-actions bot commented Feb 15, 2025 •

edited

Loading

Thmoas-Guan Feb 16, 2025 •

edited

Loading

Thmoas-Guan Feb 17, 2025 •

edited

Loading

Thmoas-Guan Feb 17, 2025 •

edited

Loading

Thmoas-Guan Feb 17, 2025 •

edited

Loading

Thmoas-Guan commented Feb 16, 2025 •

edited

Loading

Thmoas-Guan commented Feb 20, 2025 •

edited

Loading