@[simp]
theorem
AddEquiv.comp_symm
{α : Type u_1}
{β : Type u_2}
[AddZeroClass α]
[AddZeroClass β]
(e : β ≃+ α)
:
AddMonoidHom.comp ↑e ↑(AddEquiv.symm e) = AddMonoidHom.id α
@[simp]
theorem
MulEquiv.comp_symm
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(e : β ≃* α)
:
MonoidHom.comp ↑e ↑(MulEquiv.symm e) = MonoidHom.id α
theorem
Function.Injective.comp_addEquiv
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[AddZeroClass β]
[AddZeroClass γ]
[AddZeroClass δ]
(f : α → β →+ γ)
(hf : Function.Injective f)
(e : δ ≃+ β)
:
Function.Injective fun a => AddMonoidHom.comp (f a) ↑e
theorem
Function.Injective.comp_mulEquiv
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MulOneClass β]
[MulOneClass γ]
[MulOneClass δ]
(f : α → β →* γ)
(hf : Function.Injective f)
(e : δ ≃* β)
:
Function.Injective fun a => MonoidHom.comp (f a) ↑e