instHMulAwayCoeRingHomAlgebraMap — Mathlib

English

If f is surjective, then the induced map from S to Q by localization is surjective.

Русский

Если отображение f сюръективно, то индуцированное отображение S → Q локализации сюръективно.

LaTeX

$$IsLocalization.map_surjective_of_surjective _ _ _ hf$$

Lean4

/-- Localizing the localization of `R` at `x` at the image of `y` is the same as localizing
`R` at `y * x`. -/
instance (x y : R) [IsLocalization.Away x S] : IsLocalization.Away (y * x) (Localization.Away (algebraMap R S y)) :=
  IsLocalization.Away.mul S (Localization.Away (algebraMap R S y)) _ _

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