shortExact_iff_op — Mathlib

English

A short exact sequence S is short exact if and only if its opposite S.op is short exact.

Русский

Краткая точная последовательность S точна тогда и только тогда, когда противоположная последовательность S.op точна.

LaTeX

$$$ShortExact(S) \iff ShortExact(S^{op})$$$

Lean4

theorem shortExact_iff_op : S.ShortExact ↔ S.op.ShortExact :=
  ⟨ShortExact.op, ShortExact.unop⟩

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