sumDualDistrib_symm_inl — Mathlib

English

The inverse of sumDualDistrib on inl a is toDual (inl a): (sumDualDistrib α β).symm (inl (toDual a)) = toDual (inl a).

Русский

Обратное sumDualDistrib по левой части: (sumDualDistrib α β).symm (inl (toDual a)) = toDual (inl a).

LaTeX

$$$ (sumDualDistrib \alpha \beta).symm (\mathrm{inl} (\mathrm{toDual} a)) = \mathrm{toDual} (\mathrm{inl} a) $$$

Lean4

@[simp]
theorem sumDualDistrib_symm_inl : (sumDualDistrib α β).symm (inl (toDual a)) = toDual (inl a) :=
  rfl

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