[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm): rename Isometry to IsometryEquiv#6305
[Merged by Bors] - refactor(LinearAlgebra/QuadraticForm): rename Isometry to IsometryEquiv#6305eric-wieser wants to merge 6 commits intomasterfrom
Isometry to IsometryEquiv#6305Conversation
…Equiv` This is consistent with `LinearIsometryEquiv` vs `LinearIsometry`
ADedecker
left a comment
There was a problem hiding this comment.
bors d+
LGTM modulo small issue in docstrings
| #align quadratic_form.isometry QuadraticForm.IsometryEquiv | ||
|
|
||
| /-- Two quadratic forms over a ring `R` are equivalent | ||
| if there exists an isometry between them: |
There was a problem hiding this comment.
Should we replace "isometry" in these comments? We're fighting against mathematical naming issues so I don't think there's a good solution, but if you're going to introduce QuadraticForm.Isometry this might be too ambiguous.
There was a problem hiding this comment.
I've replaced them in this file. I don't think it really helps much to replace them downstream; at least, not until there is ambiguity with Isometry there.
ADedecker
left a comment
There was a problem hiding this comment.
bors d+
LGTM modulo small issue in docstrings
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Canceled. |
|
bors merge |
…Equiv` (#6305) This is consistent with `LinearIsometryEquiv` vs `LinearIsometry`. The motivation is to make room for `QuadraticForm.Isometry` as the homomorphism.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Isometry to IsometryEquivIsometry to IsometryEquiv
…Equiv` (#6305) This is consistent with `LinearIsometryEquiv` vs `LinearIsometry`. The motivation is to make room for `QuadraticForm.Isometry` as the homomorphism.
…Equiv` (#6305) This is consistent with `LinearIsometryEquiv` vs `LinearIsometry`. The motivation is to make room for `QuadraticForm.Isometry` as the homomorphism.
…Equiv` (#6305) This is consistent with `LinearIsometryEquiv` vs `LinearIsometry`. The motivation is to make room for `QuadraticForm.Isometry` as the homomorphism.
This is consistent with
LinearIsometryEquivvsLinearIsometry. The motivation is to make room forQuadraticForm.Isometryas the homomorphism.