[Merged by Bors] - chore(RepresentationTheory.GroupCohomology): make namespaces lower camel case

[101damnations]

---

Absolutely no idea why I thought these namespaces needed to be upper camel case.

[joelriou]

I am not sure that groupCohomology is better than GroupCohomology. For example, we have CategoryTheory, and not categoryTheory. Most namespaces in mathlib start with an uppercase letter:

joel@kalyani ~/lean/mathlib4 $ grep '^namespace [a-z]' **/*.lean|wc -l
130
joel@kalyani ~/lean/mathlib4 $ grep '^namespace [A-Z]' **/*.lean|wc -l
6761

(I am not sure what is the best justification for this, but it seems that lowercase initials in namespaces are used in order to develop the API around a definition which starts with a lowercase letter: for example, we have the definition of the object kernel f, and then we have kernel.lift.)

Ah, actually, in GroupCohomology.Basic, you define a term groupCohomology... Then, the namespace name change makes sense!

[101damnations]

Thank you - yeah, I've changed namespaces to lower camel when there's a definition with that name.

[digama0]

Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

[joelriou]

Thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style