[Merged by Bors] - feat: add LinearMap.IsAlt.eq_of_add_add_eq_zero#14281
[Merged by Bors] - feat: add LinearMap.IsAlt.eq_of_add_add_eq_zero#14281
LinearMap.IsAlt.eq_of_add_add_eq_zero#14281Conversation
PR summary 7857ad4e6eImport changesNo significant changes to the import graph Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
eric-wieser
left a comment
There was a problem hiding this comment.
Could you prove this for LinearMap.IsAlt too?
|
Here's a proof that works for semirings and not just rings: theorem isAlt.eq_of_add_add_eq_zero [IsCancelAdd R] {B : LinearMap.BilinForm R M} {a b c : M} (hB : B.IsAlt) (hSum : a + b + c = 0) :
B a b = B b c := by
have : B a a + B a b + B a c = B a c + B b c + B c c := by
simp_rw [← map_add, ← map_add₂, hSum, map_zero, zero_apply]
rw [hB, hB, zero_add, add_zero, add_comm] at this
exact add_left_cancel thisI'll leave adapting this to |
I naively put this above |
|
It might need to be Another trick would be to just remove that lemma from the |
|
Updated (almost no change from your suggestion, which also worked well for Actually, I don't quite understand why we don't need |
isAlt.eq_of_add_add_zeroisAlt.eq_of_add_add_eq_zero
isAlt.eq_of_add_add_eq_zeroLinearMap.IsAlt.eq_of_add_add_eq_zero
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
bors merge Thanks, this now looks great! |
For an alternating form $B : M \times M \to R$ and $a, b, c \in M$ with $a + b+ c = 0$, we have $B(a, b) = B(b, c)$. This can be used to prove the same property of Wronskian: see #14243. Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>
|
Build failed (retrying...): |
For an alternating form $B : M \times M \to R$ and $a, b, c \in M$ with $a + b+ c = 0$, we have $B(a, b) = B(b, c)$. This can be used to prove the same property of Wronskian: see #14243. Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
LinearMap.IsAlt.eq_of_add_add_eq_zeroLinearMap.IsAlt.eq_of_add_add_eq_zero
For an alternating form $B : M \times M \to R$ and $a, b, c \in M$ with $a + b+ c = 0$, we have $B(a, b) = B(b, c)$. This can be used to prove the same property of Wronskian: see #14243. Co-authored-by: Seewoo Lee <49933279+seewoo5@users.noreply.github.com>
For an alternating form$B : M \times M \to R$ and $a, b, c \in M$ with $a + b+ c = 0$ , we have $B(a, b) = B(b, c)$ .
This can be used to prove the same property of Wronskian: see #14243.