Commit 2021-10-13 15:48 a7ec6336

View on Github →

chore(algebra/*): add missing lemmas about copy on subobjects (#9624) This adds coe_copy and copy_eq to sub{mul_action,group,ring,semiring,field,module,algebra,lie_module}, to match the lemmas already present on submonoid.

Estimated changes

Modified src/algebra/algebra/subalgebra.lean

added theorem subalgebra.coe_copy

added theorem subalgebra.copy_eq

Modified src/algebra/lie/submodule.lean

added theorem lie_submodule.coe_copy

modified theorem lie_submodule.coe_submodule_injective

added theorem lie_submodule.copy_eq

Modified src/algebra/module/submodule.lean

added theorem submodule.coe_copy

added theorem submodule.copy_eq

Modified src/data/set_like/basic.lean

Modified src/field_theory/subfield.lean

added theorem subfield.coe_copy

added theorem subfield.copy_eq

Modified src/group_theory/group_action/sub_mul_action.lean

added theorem sub_mul_action.coe_copy

added theorem sub_mul_action.copy_eq

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.coe_copy

added theorem subgroup.copy_eq

Modified src/ring_theory/subring.lean

added theorem subring.coe_copy

added theorem subring.copy_eq

Modified src/ring_theory/subsemiring.lean

added theorem subsemiring.coe_copy

added theorem subsemiring.copy_eq