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 for groupCohomology.(one|two)Cocycles
  • Add groupCohomology.(one|two)Cocycles_coe_mk and groupCohomology.(one|two)Cocycles_toFun_eq_coe simp lemmas as in other FunLike types
  • Add groupCohomology.mem_(one|two)Coboundaries_iff lemmas to ease rewriting f ∈ groupCohomology.(one|two)Coboundaries into an existential statement where f is a cocycle.
  • Remove some .1 (Subtype.val) to use the FunLike instances on groupCohomology.(one|two)Cocycles Zulip thread

Estimated changes