siddhartha-gadgil on main
Removed unproven propositions Merge branch 'siddhartha-gadgil… Defined fundamental group up to… and 5 more (compare)
siddhartha-gadgil on main
removed unused variables (in co… (compare)
siddhartha-gadgil on main
no nodejs in docker (compare)
siddhartha-gadgil on main
trying codespaces (compare)
siddhartha-gadgil on main
Definitions of `Quiver` and `Se… Define additional structures Define 2-complexes and 35 more (compare)
0art0 on lean-update
0art0 on main
partial, broken update update for free groups Fix remaining upgrade errors and 1 more (compare)
0art0 on lean-update
Fix remaining upgrade errors (compare)
unit_pow_list
should first of all be camelcase as it is a definition, but also the name is cryptic. I take it this gives an element of the unit power sum from a list.Array
and use results such as Array.size_pop
.Fin
here.
unit_pow_list
takes in a list of elements of the target Abelian group and gives a function from pow_sum Unit n
(the direct sum of Unit
with itself n
times - the basis of \Z^n
) to the Abelian group where each element of pow_sum Unit n
maps to the corresponding entry in the list.
push
, pop
and size_push
, size_pop
.Fin n
is painful.
Unit^n
as a basis as we have done in the case of \Z^n
. The iterated direct sum will probably not affect the efficiency since all the computations happen with the elements of the free Abelian group, and the basis type is only used in proving that the basis elements of \Z^n
map to the chosen elements of the target Abelian group under the induced homomorphism.
Vec
(the subtype of Array
s of a fixed length) with integer entries has the structure of a free Abelian group under pointwise addition
c : Vec \Z n -> \Z ^ n
be an identification of the two types by coordinates. Once we define addition pointwise on Vec \Z n
and show that c (v + v') = c(v) + c(v')
, we can directly get a group structure on Vec \Z n
and furthermore show that it is a free Abelian group. This bypasses proofs of associativity and so on, which might be difficult with just the Array
representation.
lake init
in the ATP-Project
repo (on a separate prompts
branch), or is the Lean code for the prompts best kept separately?
theorem List.get_index_eq : (l l' : List α) → (hl : l = l') → (i : ℕ) → (bnd : i < l.length) → l.get ⟨i, bnd⟩ = l'.get ⟨i, hl ▸ bnd⟩
| _, _, rfl, _, _ => rfl