Zulip Chat Archive

Stream: maths

Topic: Bundled `lift` for `free_group`


view this post on Zulip Yury G. Kudryashov (May 24 2020 at 22:55):

I created a branch https://github.com/leanprover-community/mathlib/tree/free-group-lift with free_group.lift (former to_group) using bundled homs.

view this post on Zulip Yury G. Kudryashov (May 24 2020 at 22:55):

Help in fixing other files is very welcome but we need to coordinate.

view this post on Zulip Yury G. Kudryashov (May 24 2020 at 22:56):

I fixed up to free_abelian_group and tensor_product.

view this post on Zulip Yury G. Kudryashov (May 24 2020 at 22:57):

I've also defined free_abelian_group.ring_lift with plans to use free_monoid.lift.trans free_abelian_group.ring_lift as free_ring.lift.

view this post on Zulip Yury G. Kudryashov (May 24 2020 at 22:57):

(not done yet).

view this post on Zulip Yury G. Kudryashov (May 24 2020 at 22:58):

Unfortunately, this will lead to a large PR that can't be broken in smaller pieces.


Last updated: May 11 2021 at 16:22 UTC