Commit 2024-10-31 17:16 24ecc2ad
View on Github →chore(GroupCohomology/LowDegree): add mem_(one|two)Coboundaries_iff
(#17934)
- Add
FunLike
instances and extensionality lemmas forgroupCohomology.(one|two)Cocycles
- Add
groupCohomology.(one|two)Cocycles_coe_mk
andgroupCohomology.(one|two)Cocycles_toFun_eq_coe
simp lemmas as in otherFunLike
types - Add
groupCohomology.mem_(one|two)Coboundaries_iff
lemmas to ease rewritingf ∈ groupCohomology.(one|two)Coboundaries
into an existential statement wheref
is a cocycle. - Remove some
.1
(Subtype.val
) to use theFunLike
instances ongroupCohomology.(one|two)Cocycles
Zulip thread