inl_fst_add_inr_snd_eq — Mathlib

English

Every element of the trivial square-zero extension can be uniquely written as the sum of an inl-part and an inr-part: inl x.fst + inr x.snd = x.

Русский

Каждый элемент расширения с нулевым квадратом раскладывается uniquely как сумма части inl и inr: inl x.fst + inr x.snd = x.

LaTeX

$$$\mathrm{inl}(x.fst) + \mathrm{inr}(x.snd) = x$$$

Lean4

theorem inl_fst_add_inr_snd_eq [AddZeroClass R] [AddZeroClass M] (x : tsze R M) : inl x.fst + inr x.snd = x :=
  ext (add_zero x.1) (zero_add x.2)

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