associated_sec_fst — Mathlib

English

In Away localization, algebraMap y is a unit iff y divides a power of x.

Русский

ВAway-локализации алгебраMap y — единица тогда и только тогда, когда y делит некоторую степень x.

LaTeX

$$algebraMap_isUnit_iff {y : R} : IsUnit (algebraMap R S y) ↔ ∃ n, y ∣ x ^ n$$

Lean4

theorem associated_sec_fst (s : S) : Associated (algebraMap R S (IsLocalization.Away.sec x s).1) s :=
  by
  rw [← IsLocalization.Away.sec_spec, map_pow]
  exact associated_mul_unit_left _ _ <| .pow _ <| IsLocalization.Away.algebraMap_isUnit _

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