English
Assuming G finite, there is a finite type structure on the elements of vectorsProdEqOne G n.
Русский
При конечности группы G существует конечный тип элементов множества vectorsProdEqOne G n.
LaTeX
$$Fintype (Equiv.Perm.vectorsProdEqOne G n).Elem$$
Lean4
/-- Given a vector `v` of length `n`, make a vector of length `n + 1` whose product is `1`,
by appending the inverse of the product of `v`. -/
@[simps]
def vectorEquiv : List.Vector G n ≃ vectorsProdEqOne G (n + 1)
where
toFun v := ⟨v.toList.prod⁻¹ ::ᵥ v, by rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_cancel]⟩
invFun v := v.1.tail
left_inv v := v.tail_cons v.toList.prod⁻¹
right_inv
v :=
Subtype.ext <|
calc
v.1.tail.toList.prod⁻¹ ::ᵥ v.1.tail = v.1.head ::ᵥ v.1.tail :=
congr_arg (· ::ᵥ v.1.tail) <|
Eq.symm <|
eq_inv_of_mul_eq_one_left <|
by
rw [← List.prod_cons, ← Vector.toList_cons, v.1.cons_head_tail]
exact v.2
_ = v.1 := v.1.cons_head_tail
