Commit 2021-11-08 08:27 380d6cae

View on Github →

chore(algebra/direct_sum/module): extract out common variables (#10207) Slight reorganization to extract out repeatedly-used variable declarations, and update module docstring. No changes to the content.

Estimated changes

Modified src/algebra/direct_sum/module.lean

modified def direct_sum.submodule_coe

modified theorem direct_sum.submodule_coe_of

modified theorem direct_sum.submodule_is_internal.independent

modified theorem direct_sum.submodule_is_internal.supr_eq_top

modified theorem direct_sum.submodule_is_internal.to_add_subgroup

modified theorem direct_sum.submodule_is_internal.to_add_submonoid

modified def direct_sum.submodule_is_internal

modified theorem direct_sum.submodule_is_internal_iff_independent_and_supr_eq_top

modified theorem direct_sum.submodule_is_internal_of_independent_of_supr_eq_top