compl₂_id — Mathlib

English

If two bilinear maps are equal, then they yield equal values when evaluated at any pair of inputs.

Русский

Если две билинейные карты равны, то они дают одинаковые значения на любых входах.

LaTeX

$$$$ f = g \Rightarrow f x y = g x y $$$$

Lean4

@[simp]
theorem compl₂_id (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) : h.compl₂ LinearMap.id = h :=
  by
  ext
  rw [compl₂_apply, id_coe, _root_.id]

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