Nielson Transformations

Stream: Is there code for X?

[Suryansh Shrivastava]

Does there exist Nielsen transformations in mathlib? If not, is it a good idea to formalize it?

[Kim Morrison]

We have https://leanprover-community.github.io/mathlib4_docs/find/?pattern=subgroupIsFreeOfIsFree#doc

[Kim Morrison]

Sadly neither moogle.ai nor leansearch.net find that, which is a bit disappointing.

[Kim Morrison]

But grep, or VSCode search, work well for queries like this.