biprod_isZero_iff — Mathlib

English

IsZero (biprod A B) iff IsZero A ∧ IsZero B.

Русский

IsZero (биобразование A B) эквивалентно IsZero A ∧ IsZero B.

LaTeX

$$$\operatorname{IsZero}(\mathrm{biprod} A B) \iff \big( \operatorname{IsZero} A \land \operatorname{IsZero} B \big)$$$

Lean4

@[simp]
theorem biprod_isZero_iff (A B : C) [HasBinaryBiproduct A B] : IsZero (biprod A B) ↔ IsZero A ∧ IsZero B :=
  by
  constructor
  · intro h
    simp only [IsZero.iff_id_eq_zero] at h ⊢
    simp only [show 𝟙 A = biprod.inl ≫ 𝟙 (A ⊞ B) ≫ biprod.fst by simp,
      show 𝟙 B = biprod.inr ≫ 𝟙 (A ⊞ B) ≫ biprod.snd by simp, h, zero_comp, comp_zero, and_self]
  · rintro ⟨hA, hB⟩
    rw [IsZero.iff_id_eq_zero]
    apply biprod.hom_ext
    · apply hA.eq_of_tgt
    · apply hB.eq_of_tgt

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