siddhartha-gadgil on v2.0-uc
siddhartha-gadgil on unit-conjecture
fun not lambdas Merge branch 'unit-conjecture' … (compare)
0art0 on unit-conjecture
Change from `\lambda` to `fun` … (compare)
siddhartha-gadgil on unit-conjecture
removing unused variables (compare)
0art0 on unit-conjecture
Change quotes to italics Indentation fix (compare)
0art0 on unit-conjecture
Push trivial proofs out of `Tor… Merge branch 'unit-conjecture' … (compare)
siddhartha-gadgil on unit-conjecture
comment tweaked (compare)
siddhartha-gadgil on unit-conjecture
tweak Merge branch 'unit-conjecture' … (compare)
0art0 on unit-conjecture
Change `apply Q.rec` -> `cases … (compare)
0art0 on unit-conjecture
Improved documentation for the … Merge documentation Add more documentation and 1 more (compare)
siddhartha-gadgil on unit-conjecture
corrected silly CI (compare)
siddhartha-gadgil on unit-conjecture
FreeModule sections (compare)
siddhartha-gadgil on unit-conjecture
headings in top docs (compare)
siddhartha-gadgil on unit-conjecture
top docs for all files, docs fo… (compare)
siddhartha-gadgil on unit-conjecture
Modify CI Modify CI further Make elan path explicit and 3 more (compare)
siddhartha-gadgil on main
CI tweak (compare)
siddhartha-gadgil on unit-conjecture
CI tweak Merge branch 'unit-conjecture' … (compare)
0art0 on main
Try building the mathlib folder… (compare)
0art0 on main
Make elan path explicit (compare)
0art0 on main
Modify CI further (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