Skip to content

Conversation

@themathqueen
Copy link
Collaborator

@themathqueen themathqueen commented Jan 23, 2026

I forgot to update the hypotheses when I changed it to LinearEquiv from LinearIsometryEquiv.

I also removed the TODO since I'm not convinced we should have them all on one type anymore. For example we have the algebra instances on n -> R and the Hilbert space on EuclideanSpace. Even though we could technically introduce the algebra instances on this Hilbert space, we probably shouldn't be doing that.


Open in Gitpod

@themathqueen themathqueen requested a review from ocfnash January 23, 2026 21:34
@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Jan 23, 2026
@github-actions
Copy link

github-actions bot commented Jan 23, 2026

PR summary cb6b2796fb

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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).

@themathqueen themathqueen changed the title chore(Analysis/InnerProductSpace/Coalgebra): generalize from NormedRing to Semiring chore(Analysis/InnerProductSpace/Coalgebra): generalize from NormedRing to Ring Jan 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants