[Merged by Bors] - feat: add LinearMap.IsAlt.eq_of_add_add_eq_zero

[seewoo5]

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.

---

[github-actions]

PR summary 7857ad4e6e

Import changes

No significant changes to the import graph

---

Declarations diff

+ IsAlt.eq_of_add_add_eq_zero
+ eq_of_add_add_eq_zero

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]

Could you prove this for LinearMap.IsAlt too?

[eric-wieser]

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 this

I'll leave adapting this to LinearMap.IsAlt to you :)

[seewoo5]

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 this

I'll leave adapting this to LinearMap.IsAlt to you :)

I naively put this above end IsAlt as theorem eq_of_add_add_eq_zero ..., and it says that zero_apply in simp_rw made no progress. Do you have any idea?

[eric-wieser]

It might need to be LinearMap.zero_apply. If you push what you tried, I can help more.

Another trick would be to just remove that lemma from the simp_rw, then use simp? to find what the lemma is really called.

[seewoo5]

Updated (almost no change from your suggestion, which also worked well for LinearMap.IsAlt. I changed some names of variables and remove unnecessary terms, too.

Actually, I don't quite understand why we don't need IsCancelAdd R₁ hypothesis for the same theorem in SesquilinearForm.lean. I was not able to find the relevant assumption in the file, but it works well without explicitly assuming it in the theorem, so I guess I'm missing the hypothesis which is somewhere in the file.

[eric-wieser]

bors merge

Thanks, this now looks great!

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style