Richard Copley comments

Results 12 comments of


                                            Richard Copley

`std::coroutines` in INTERFACE_LINK_LIBRARIES breaks cmake packages that consume libunifex

Correction: the find module should not be `include`d. It is for `find_package`, when operating in module mode. Instead, save the find module in the consuming project as `cmake/find/Findunifex.cmake`. Add the...

Fix magit-section usage so the expand/contract functionality works

force-push: rebase onto #51

Fix magit-section usage so the expand/contract functionality works

Rebased onto [leanprover-community:master](https://github.com/leanprover-community/lean4-mode/tree/master)

Fix magit-section usage so the expand/contract functionality works

I see no reason not to. It's just a minor bugfix. @sebeaumont, please ping Yury (@urkud) on Zulip.

Go over suggestions in #51

#### First change (in `lean4-lake-find-dir` in "lean4-lake.el"): I agree with the change but I also wonder if anyone would notice if we deleted "lean4-lake.el". We could just mention in the...

A lemma of B. H. Neumann.

Moved to #13047

feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann)

Thanks for the review, @alreadydone. I'll have a go at the corollary you stated, but probably nothing stronger for now.

feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann)

[Edited] Do you have any opinion on where `Subspace.biUnion_ne_univ_of_lt_top` (signature below) should go? For my part I think it's ok here in `GroupTheory.CosetCover`, as a corollary. Alternatives: * `LinearAlgebra.Basis.VectorSpace` (for...

feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann)

> [Here](https://github.com/leanprover-community/mathlib4/commit/ab3feb84d91f43a7ec55ef93a28e396e71e907b3) are some slight golf and a rephrase of the vector space result Thank you, I pushed those.

feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann)

> The pr is very close to proving disjointness of cosets when the density equals one. It might however be necessary to refactor the intermediate construction to transfer more properties...