congrRight₂_apply — Mathlib

English

If B1 and B2 become equal after left-right transformation by surjective l and r, then B1 = B2.

Русский

Если B1 и B2 становятся равными после преобразования слева и справа с сюрьективными l и r, то B1 = B2.

LaTeX

$$B1.comp l r = B2.comp l r → B1 = B2$$

Lean4

@[simp]
theorem _root_.LinearEquiv.congrRight₂_apply (e : N₁ ≃ₗ[R] N₂) (B : BilinMap R M N₁) :
    LinearEquiv.congrRight₂ e B = compr₂ B e :=
  rfl

Похожие утверждения