compl₁₂_id_id — Mathlib

English

Let f be a bilinear map f: M → N → P. Then composing f with the identity maps on M and N leaves f unchanged; i.e. f composed with id_M and id_N equals f.

Русский

Пусть f — билинейное отображение f: M → N → P. Тогда композиция f с тождественными отображениями по обеим переменным не меняет её: f = f ∘ (id_M, id_N).

LaTeX

$$$f = f \circ (\mathrm{id}_M, \mathrm{id}_N).$$$$

Lean4

@[simp]
theorem compl₁₂_id_id [SMulCommClass R₂ R₁ Pₗ] (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) : f.compl₁₂ LinearMap.id LinearMap.id = f :=
  by
  ext
  simp_rw [compl₁₂_apply, id_coe, _root_.id]

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