Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-01 07:01 85fe90e9

View on Github →

feat(algebra/direct_sum/module) : coe and internal (#10004) This extracts the following defs from within the various is_internal properties:

  • direct_sum.add_submonoid_coe
  • direct_sum.add_subgroup_coe
  • direct_sum.submodule_coe Packing these into a def makes things more concise, and avoids some annoying elaboration issues.

Estimated changes