Commit 2023-10-23 14:19 f977d712

View on Github →

chore(RepresentationTheory.GroupCohomology): make namespaces lower camel case (#6029)

Estimated changes

Modified Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

deleted def GroupCohomology.inhomogeneousCochainsIso

deleted theorem GroupCohomology.linearYonedaObjResolution_d_apply

deleted def InhomogeneousCochains.d

deleted theorem InhomogeneousCochains.d_eq

added def groupCohomology.inhomogeneousCochainsIso

added theorem groupCohomology.linearYonedaObjResolution_d_apply

added def inhomogeneousCochains.d

added theorem inhomogeneousCochains.d_eq

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

deleted def GroupCohomology.Resolution.actionDiagonalSucc

deleted theorem GroupCohomology.Resolution.actionDiagonalSucc_hom_apply

deleted theorem GroupCohomology.Resolution.actionDiagonalSucc_inv_apply

deleted def GroupCohomology.Resolution.compForgetAugmentedIso

deleted def GroupCohomology.Resolution.d

deleted theorem GroupCohomology.Resolution.d_comp_ε

deleted theorem GroupCohomology.Resolution.d_eq

deleted theorem GroupCohomology.Resolution.d_of

deleted def GroupCohomology.Resolution.diagonalSucc

deleted theorem GroupCohomology.Resolution.diagonalSucc_hom_single

deleted theorem GroupCohomology.Resolution.diagonalSucc_inv_single_left

deleted theorem GroupCohomology.Resolution.diagonalSucc_inv_single_right

deleted theorem GroupCohomology.Resolution.diagonalSucc_inv_single_single

deleted def GroupCohomology.Resolution.forget₂ToModuleCat

deleted def GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv

deleted theorem GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv_f_0_eq

deleted def GroupCohomology.Resolution.ofMulActionBasis

deleted def GroupCohomology.Resolution.ofMulActionBasisAux

deleted theorem GroupCohomology.Resolution.ofMulAction_free

deleted theorem GroupCohomology.Resolution.quasiIsoOfForget₂εToSingle₀

deleted def GroupCohomology.Resolution.xIso

deleted theorem GroupCohomology.Resolution.x_projective

deleted def GroupCohomology.Resolution.ε

deleted def GroupCohomology.Resolution.εToSingle₀

deleted theorem GroupCohomology.Resolution.εToSingle₀_comp_eq

deleted def GroupCohomology.extIso

deleted def GroupCohomology.projectiveResolution

deleted def GroupCohomology.resolution

added def groupCohomology.extIso

added def groupCohomology.projectiveResolution

added def groupCohomology.resolution.actionDiagonalSucc

added theorem groupCohomology.resolution.actionDiagonalSucc_hom_apply

added theorem groupCohomology.resolution.actionDiagonalSucc_inv_apply

added def groupCohomology.resolution.compForgetAugmentedIso

added def groupCohomology.resolution.d

added theorem groupCohomology.resolution.d_comp_ε

added theorem groupCohomology.resolution.d_eq

added theorem groupCohomology.resolution.d_of

added def groupCohomology.resolution.diagonalSucc

added theorem groupCohomology.resolution.diagonalSucc_hom_single

added theorem groupCohomology.resolution.diagonalSucc_inv_single_left

added theorem groupCohomology.resolution.diagonalSucc_inv_single_right

added theorem groupCohomology.resolution.diagonalSucc_inv_single_single

added def groupCohomology.resolution.forget₂ToModuleCat

added def groupCohomology.resolution.forget₂ToModuleCatHomotopyEquiv

added theorem groupCohomology.resolution.forget₂ToModuleCatHomotopyEquiv_f_0_eq

added def groupCohomology.resolution.ofMulActionBasis

added def groupCohomology.resolution.ofMulActionBasisAux

added theorem groupCohomology.resolution.ofMulAction_free

added theorem groupCohomology.resolution.quasiIsoOfForget₂εToSingle₀

added def groupCohomology.resolution.xIso

added theorem groupCohomology.resolution.x_projective

added def groupCohomology.resolution.ε

added def groupCohomology.resolution.εToSingle₀

added theorem groupCohomology.resolution.εToSingle₀_comp_eq

added def groupCohomology.resolution