Commit 2021-11-08 14:15 5ba41d8f

View on Github →

feat(algebra/direct_sum): specialize submodule_is_internal.independent to add_subgroup (#10108) This adds the lemmas disjoint.map_order_iso and complete_lattice.independent.map_order_iso (and iff versions), and uses them to transfer some results on submodules to add_submonoids and add_subgroups.

Estimated changes

Modified src/algebra/direct_sum/module.lean

added theorem direct_sum.add_subgroup_is_internal.independent

added theorem direct_sum.add_submonoid_is_internal.independent

Modified src/linear_algebra/dfinsupp.lean

added theorem complete_lattice.independent.dfinsupp_sum_add_hom_injective

added theorem complete_lattice.independent_iff_dfinsupp_sum_add_hom_injective

added theorem complete_lattice.independent_of_dfinsupp_sum_add_hom_injective'

added theorem complete_lattice.independent_of_dfinsupp_sum_add_hom_injective

Modified src/order/complete_lattice.lean

added theorem complete_lattice.independent.map_order_iso

added theorem complete_lattice.independent_map_order_iso_iff

Modified src/order/rel_iso.lean

added theorem disjoint.map_order_iso

added theorem disjoint_map_order_iso_iff