bijective_algebraMap_of_subsingleton_units_mrange

English

For a valuation v on F with integers O, IsUnit x iff v(algebraMap x) = 1.

Русский

Для оценки v на F с целыми O, x является единицей тогда и только тогда, когда v(алгебраMap(O,F)(x)) = 1.

LaTeX

$$$\text{IsUnit}(x) \iff v(\mathrm{algebraMap}(O,F)(x)) = 1$$$

Lean4

theorem bijective_algebraMap_of_subsingleton_units_mrange (hv : Integers v O) [Subsingleton (MonoidHom.mrange v)ˣ] :
    Function.Bijective (algebraMap O F) :=
  by
  refine ⟨hv.hom_inj, fun x ↦ hv.exists_of_le_one ?_⟩
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  ·
    exact
      (congr_arg Units.val
          (Subsingleton.elim (α := (MonoidHom.mrange v)ˣ)
            ((isUnit_iff_ne_zero.mpr hx).unit.map v.toMonoidHom.mrangeRestrict) 1)).le

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