Mathlib Changelog
v4
Changelog
About
Github
Theorem
QuotientGroup.mk'_comp_subtype
Modification history
2025-05-29 17:22
Mathlib/GroupTheory/QuotientGroup/Defs.lean
feat(RepresentationTheory/GroupCohomology/Functoriality): the degree 1 part of the inflation-restriction exact sequence (#22653) …
Added
QuotientGroup.mk'_comp_subtype
View on Github →