Skip to content

[Merged by Bors] - feat: algebraic operations on SeparationQuotient _#12329

Closed
urkud wants to merge 16 commits intomasterfrom
YK-sep-quot-mul
Closed

[Merged by Bors] - feat: algebraic operations on SeparationQuotient _#12329
urkud wants to merge 16 commits intomasterfrom
YK-sep-quot-mul

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Apr 22, 2024 •
edited by github-actions bot
Loading

I need this to drop [T2Space _] assumptions here and there.

I don't know if I should break it into smaller pieces with fewer dependencies for anything by the CLM part.

Open in Gitpod

urkud added 4 commits April 15, 2024 01:11
@urkud
Snapshot
f00d2c7
@urkud
feat(Inseparable): Prod.map mk mk is a quotient map
7c21b20 
This is needed to prove continuity of binary arithmetic operations
on the separation quotient.
@urkud
Merge branch 'YK-sepquot-prodmap' into YK-sep-quot-mul
4fa0aea
@urkud
Update
4421597
@urkud urkud changed the title Snapshot feat: algebraic operations on SeparationQuotient _ Apr 22, 2024
@urkud urkud added WIP Work in progress t-topology Topological spaces, uniform spaces, metric spaces, filters t-algebra Algebra (groups, rings, fields, etc) labels Apr 22, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 22, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 23, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 8, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 15, 2024 •
edited
Loading

PR summary 147ea065b4

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Topology.Algebra.SeparationQuotient 1038

Declarations diff

+ exists_out_continuousLinearMap
+ instCommGroup
+ instCommMagma
+ instCommMonoid
+ instCommMonoidWithZero
+ instCommRing
+ instCommSemigroup
+ instCommSemiring
+ instContinuousConstSMul
+ instContinuousDiv
+ instContinuousInv
+ instContinuousMul
+ instDistrib
+ instDistribMulAction
+ instDistribSMul
+ instDiv
+ instGroup
+ instHasDistribNeg
+ instIntCast
+ instInv
+ instInvOneClass
+ instInvolutiveInv
+ instIsCentralScalar
+ instIsPretransitiveSMul
+ instIsScalarTower
+ instLeftDistribClass
+ instModule
+ instMonoid
+ instMonoidWithZero
+ instMul
+ instMulAction
+ instMulDistribMulAction
+ instMulOneClass
+ instMulZeroClass
+ instMulZeroOneClass
+ instNatCast
+ instNonAssocRing
+ instNonAssocSemiring
+ instNonUnitalCommRing
+ instNonUnitalCommSemiring
+ instNonUnitalNonAssocCommRing
+ instNonUnitalNonAssocCommSemiring
+ instNonUnitalNonAssocRing
+ instNonUnitalRing
+ instNonUnitalSemiring
+ instNonUnitalnonAssocSemiring
+ instPow
+ instRightDistribClass
+ instRing
+ instSMul
+ instSMulCommClass
+ instSMulZeroClass
+ instSemigroup
+ instSemigroupWithZero
+ instSemiring
+ instZPow
+ instZSMul
+ instance (priority := 900) instNSmul [AddMonoid M] [ContinuousAdd M] :
+ instance [One X] : One (SeparationQuotient X) := ⟨mk 1⟩
+ mkCLM
+ mkCLM_comp_outCLM
+ mkMonoidHom
+ mk_comp_outCLM
+ mk_div
+ mk_intCast
+ mk_inv
+ mk_mul
+ mk_natCast
+ mk_ofNat
+ mk_one
+ mk_outCLM
+ mk_pow
+ mk_smul
+ mk_zpow
+ outCLM
+ outCLM_embedding
+ outCLM_injective
+ outCLM_uniformContinuous
+ outCLM_uniformEmbedding
+ outCLM_uniformInducing

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>

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 15, 2024
@urkud urkud removed the WIP Work in progress label Jul 15, 2024
@urkud urkud marked this pull request as ready for review July 15, 2024 14:26
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 15, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 15, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jul 15, 2024

This PR/issue depends on:

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 15, 2024
@urkud urkud removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 15, 2024
jcommelin
jcommelin reviewed Aug 23, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Aug 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 23, 2024
@urkud
feat: algebraic operations on SeparationQuotient _ (#12329)
05827b1 
I need this to drop `[T2Space _]` assumptions here and there.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: algebraic operations on SeparationQuotient _ [Merged by Bors] - feat: algebraic operations on SeparationQuotient _ Aug 23, 2024
@mathlib-bors mathlib-bors bot closed this Aug 23, 2024
@mathlib-bors mathlib-bors bot deleted the YK-sep-quot-mul branch August 23, 2024 11:17
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@urkud @bjoernkjoshanssen
feat: algebraic operations on SeparationQuotient _ (#12329)
8b3af29 
I need this to drop `[T2Space _]` assumptions here and there.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@urkud @bjoernkjoshanssen
feat: algebraic operations on SeparationQuotient _ (#12329)
e79709e 
I need this to drop `[T2Space _]` assumptions here and there.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@urkud @bjoernkjoshanssen
feat: algebraic operations on SeparationQuotient _ (#12329)
aa7a6ea 
I need this to drop `[T2Space _]` assumptions here and there.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@urkud @jcommelin