MulEquiv.ofInjective' #
An injective monoid homomorphism is a MulEquiv onto its range — the MulOneClass
counterpart of the group-level MonoidHom.ofInjective, packaging MulEquiv.ofLeftInverse'
at an injectivity hypothesis. Primed like MulEquiv.ofLeftInverse': the unprimed name is
reserved for the f.range version.
noncomputable def
MulEquiv.ofInjective'
{M : Type u_1}
{N : Type u_2}
[MulOneClass M]
[MulOneClass N]
{f : M →* N}
(hf : Function.Injective ⇑f)
:
M ≃* ↥(MonoidHom.mrange f)
An injective monoid homomorphism is a MulEquiv onto its range — the MulOneClass
counterpart of MonoidHom.ofInjective.
Equations
- MulEquiv.ofInjective' hf = MulEquiv.ofLeftInverse' f ⋯
Instances For
noncomputable def
AddEquiv.ofInjective'
{M : Type u_1}
{N : Type u_2}
[AddZeroClass M]
[AddZeroClass N]
{f : M →+ N}
(hf : Function.Injective ⇑f)
:
M ≃+ ↥(AddMonoidHom.mrange f)
An injective additive monoid homomorphism is an AddEquiv onto its
range.
Equations
- AddEquiv.ofInjective' hf = AddEquiv.ofLeftInverse' f ⋯