-
Notifications
You must be signed in to change notification settings - Fork 330
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
refactor(LinearAlgebra/BilinearForm/TensorProduct): Tensor products of bilinear maps #14988
base: master
Are you sure you want to change the base?
Conversation
PR summary 21ea33a912
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.LinearAlgebra.BilinearForm.TensorProduct | 1275 | 1277 | +2 (+0.16%) |
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct | 1308 | 1310 | +2 (+0.15%) |
Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange | 1325 | 1327 | +2 (+0.15%) |
Import changes for all files
Files | Import difference |
---|---|
6 filesMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries |
2 |
Declarations diff
+ exists_quadraticMap_ne_zero
++ tensorDistrib
++ tensorDistrib_tmul
++- baseChange
++- baseChange_tmul
+-++ tmul
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.
CC: @eric-wieser |
@eric-wieser did you have any further thoughts on this please? |
Co-authored-by: Eric Wieser <efw@google.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you fill out the "moves" section of the PR template to indicate that BilinMap.tmul
and friends have moved to BilinForm.tmul
?
Co-authored-by: Eric Wieser <efw@google.com>
Extend the results in
Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
from Bilinear Forms to Bilinear MapsSimilarly for
LinearAlgebra/QuadraticForm/TensorProduct
.I had originally intended to extend much more, but was blocked by not being able to extend
LinearMap.IsSymm
from forms to maps.LinearEquiv.congrQuadraticMap
andLinearEquiv.congrRight₂
#17454