English
If bilinear forms B1 and B2 become equal after applying the same left and right linear maps l and r with surjective l and r, then B1 = B2.
Русский
Если билинейные формы B1 и B2 становятся равными после применения одинаковых слева и справа отображений l и r, где l и r сюрьективны, тогда B1 = B2.
LaTeX
$$For all B1,B2, l,r with surjective l,r, (B1.comp l r) = (B2.comp l r) ↔ B1 = B2$$
Lean4
theorem comp_inj (B₁ B₂ : BilinForm R M') {l r : M →ₗ[R] M'} (hₗ : Function.Surjective l) (hᵣ : Function.Surjective r) :
B₁.comp l r = B₂.comp l r ↔ B₁ = B₂ := by
constructor <;> intro h
· -- B₁.comp l r = B₂.comp l r → B₁ = B₂
ext x y
obtain ⟨x', hx⟩ := hₗ x
subst hx
obtain ⟨y', hy⟩ := hᵣ y
subst hy
rw [← comp_apply, ← comp_apply, h]
· -- B₁ = B₂ → B₁.comp l r = B₂.comp l r
rw [h]
