ext

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.ext

English

Two elements of TrivSqZeroExt R M are equal iff their fst and snd components are equal.

Русский

Два элемента TrivSqZeroExt R M равны тогда и только тогда, когда их первые и вторые компоненты совпадают.

LaTeX

$$x = y ↔ (x.fst = y.fst ∧ x.snd = y.snd)$$

Lean4

@[ext]
theorem ext {x y : tsze R M} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) : x = y :=
  Prod.ext h1 h2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru