English
A division-monoid M with a topology yields an embedding of the units into M whenever Inv is continuous on units.
Русский
Для моноида с делением и топологией вложение единиц в M является вложением, если Inv непрерывно на единицах.
LaTeX
$$$\\text{IsEmbedding}(\\mathrm{val} : M^\\times \\to M)$$$
Lean4
/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead. -/
@[to_additive /-- An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a
topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead. -/
]
theorem embedding_val_mk {M : Type*} [DivisionMonoid M] [TopologicalSpace M]
(h : ContinuousOn Inv.inv {x : M | IsUnit x}) : IsEmbedding (val : Mˣ → M) :=
isEmbedding_val_mk' h fun u ↦ (val_inv_eq_inv_val u).symm
