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
[Merged by Bors] - feat: port LinearAlgebra.SesquilinearForm #2607
Conversation
ocfnash
commented
Mar 3, 2023
/-- A set of vectors `v` is orthogonal with respect to some bilinear form `B` if and only | ||
if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two elements, use | ||
`bilin_form.is_ortho` -/ | ||
def IsOrthoCat (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R) (v : n → M₁) : Prop := |
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.
Unfortunately the original Mathlib3 source commits the sin of having two definitions with names distinguished only by case:
linear_map.is_ortho
linear_map.is_Ortho
It seems Mathport deals with this by naming them LinearMap.IsOrtho
and LinearMap.IsOrthoCat
respectively. I'm not sure if we should first rename in Mathlib3 or just rename on the fly.
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.
I have taken the liberty of simply renaming these on the fly to LinearMap.IsOrtho
and LinearMap.IsOrthoᵢ
so as to match other things that have binary and indexed versions (like sup
and supᵢ
or union
and unionᵢ
).
@ocfnash The errors here are definitely caused by lean4#2074 because the file compiles with
Unfortunately I have to stop working on this for now though. I didn't push any fixes yet, just wanted to document them here. |
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
That's is for today
This is horrible. I think it's better to wait and see if we solve these issues more generally before putting more time into this file.
I still need `set_option synthInstance.etaExperiment true` to get things to work but hopefully we can solve this next.
With these changes, this will now build provided we add: `set_option synthInstance.etaExperiment true` Unfortunately I haven't found a way to avoid using this yet.
8d478b1
to
4811df5
Compare
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.
Thanks 🎉
bors merge
Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Pull request successfully merged into master. Build succeeded:
|