idemFst_add_idemSnd — Mathlib

English

idemFst x equals toLp p (x.fst, 0) by definition.

Русский

idemFst x равно toLp p (x.fst, 0) по определению.

LaTeX

$$$\mathrm{idemFst}\,x = \mathrm{toLp}(p)(x_1,0).$$$

Lean4

@[simp]
theorem idemFst_add_idemSnd : idemFst + idemSnd = (1 : AddMonoid.End (WithLp p (α × β))) :=
  AddMonoidHom.ext fun x =>
    by
    rw [AddMonoidHom.add_apply, idemFst_apply, idemSnd_apply, AddMonoid.End.coe_one, id_eq, ← toLp_add, Prod.mk_add_mk,
      zero_add, add_zero]
    rfl

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