English
A property P of ring homs holds for R → S whenever there exists a spanning set for S such that P holds for R → S_r for each r in the set.
Русский
Свойство P гомоморфизмов кольца выполняется для R → S, если существует порождающий набор для S такой, что P выполняется для R → S_r для каждого r.
LaTeX
$$$\\forall s \\subseteq S \\, (\\forall r \\in s, P((\\mathrm{algebraMap}\\, S\\to_S) \\circ f)) \\Rightarrow P(f).$$$
Lean4
/-- A property `P` of ring homs satisfies `RingHom.OfLocalizationFiniteSpan`
if `P` holds for `R →+* S` whenever there exists a set `{ r }` that spans `R` such that
`P` holds for `Rᵣ →+* Sᵣ`.
Note that this is equivalent to `RingHom.OfLocalizationFiniteSpan` via
`RingHom.ofLocalizationSpan_iff_finite`, but this has less restrictions when applying. -/
def OfLocalizationSpan :=
∀ ⦃R S : Type u⦄ [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (_ : Ideal.span s = ⊤)
(_ : ∀ r : s, P (Localization.awayMap f r)), P f
