ext

Mathlib.RingTheory.WittVector.Truncated

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

English

TruncatedWittVector obeys extensionality: equality is determined componentwise.

Русский

Extensionality для TruncatedWittVector: равенство определяется покомпонентно.

LaTeX

$$$\\forall x,y : TruncatedWittVector\\ p\\ n\\ R,\\; (\\forall i : Fin n, x.coeff i = y.coeff i) \\Rightarrow x = y$$$

Lean4

@[ext]
theorem ext {x y : TruncatedWittVector p n R} (h : ∀ i, x.coeff i = y.coeff i) : x = y :=
  funext h

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

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

Разделы

Аффилиация

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