map_isUnit_of_le — Mathlib

English

If S ≤ A⁰, then for any s ∈ S, algebraMap A K s is a unit in K (via Localization).

Русский

Если $S \\le A^0$, то для любого $s\\in S$ элемент $\\mathrm{algebraMap} \\, A K s$ является единицей в $K$ (через локализацию).

LaTeX

$$$S \\le A^{0} \\Rightarrow \\forall s \\in S, IsUnit(\\mathrm{algebraMap}_{AK}(s))$$$

Lean4

theorem map_isUnit_of_le (hS : S ≤ A⁰) (s : S) : IsUnit (algebraMap A K s) := by
  apply IsLocalization.map_units K (⟨s.1, hS s.2⟩ : A⁰)

Похожие утверждения