codRestrictOfInjective_comp — Mathlib

English

For the restricted bilinear map codRestrict₂, applying i to its output yields the original value f x y.

Русский

Для ограниченного билинейного отображения codRestrict₂ применение i к результату даёт исходное значение f x y.

LaTeX

$$$i (codRestrict₂ f i hi hf x y) = f x y$$$

Lean4

@[simp]
theorem codRestrictOfInjective_comp : i ∘ₗ LinearMap.codRestrictOfInjective f i hi hf = f :=
  by
  ext
  simp

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