fst_comp_inl — Mathlib

English

The composition of the first projection with the left-inclusion into the product is the identity on the first component.

Русский

Составление проекции fst с левого включения в произведение дает тождество на первом компоненте.

LaTeX

$$$(\mathrm{fst}\; M_2\; Q_1) \circ (\mathrm{inl}\; Q_1\; (0)) = \mathrm{id}_{Q_1}$$$

Lean4

@[simp]
theorem fst_comp_inl (Q₁ : QuadraticMap R M₁ P) : (fst M₂ Q₁).comp (inl Q₁ (0 : QuadraticMap R M₂ P)) = .id _ :=
  ext fun _ => rfl

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