Commit 2022-01-05 14:15 57a9f8be

View on Github →

chore(group_theory/sub{monoid,group}, linear_algebra/basic): rename equivalences to mapped subobjects (#11075) This makes the names shorter and more uniform:

add_equiv.map_add_submonoid
add_equiv.map_add_subgroup
linear_equiv.map_submodule

Estimated changes

Modified src/algebra/lie/subalgebra.lean

added def lie_equiv.lie_subalgebra_map

added theorem lie_equiv.lie_subalgebra_map_apply

deleted def lie_equiv.of_subalgebra

deleted theorem lie_equiv.of_subalgebra_apply

Modified src/group_theory/group_action/basic.lean

Modified src/group_theory/subgroup/basic.lean

deleted def mul_equiv.subgroup_equiv_map

added def mul_equiv.subgroup_map

Modified src/group_theory/subgroup/pointwise.lean

Modified src/group_theory/submonoid/operations.lean

deleted def mul_equiv.submonoid_equiv_map

added def mul_equiv.submonoid_map

Modified src/linear_algebra/basic.lean

deleted def linear_equiv.of_submodule

deleted theorem linear_equiv.of_submodule_apply

deleted theorem linear_equiv.of_submodule_symm_apply

added def linear_equiv.submodule_map

added theorem linear_equiv.submodule_map_apply

added theorem linear_equiv.submodule_map_symm_apply

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/finite_dimensional.lean