one_eq — Mathlib

English

There is a unique 0-length vector in vectorsProdEqOne(G,0).

Русский

Существует единственный нулевой вектор в vectorsProdEqOne(G,0).

LaTeX

$$There is a unique element of vectorsProdEqOne(G,0).$$

Lean4

theorem one_eq : vectorsProdEqOne G 1 = {Vector.nil.cons 1} :=
  by
  simp_rw [Set.eq_singleton_iff_unique_mem, mem_iff, List.Vector.toList_singleton, List.prod_singleton,
    List.Vector.head_cons, true_and]
  exact fun v hv => v.cons_head_tail.symm.trans (congr_arg₂ Vector.cons hv v.tail.eq_nil)

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