preValuationRing — Mathlib

English

If f: R →* S is a surjective multiplicative homomorphism and R has a PreValuationRing structure, then S also has a PreValuationRing structure.

Русский

Если f: R →* S сюръективен и R имеет структуру PreValuationRing, то и S имеет структуру PreValuationRing.

LaTeX

$$$\\text{PreValuationRing } S$$$

Lean4

theorem _root_.Function.Surjective.preValuationRing {R S : Type*} [Mul R] [PreValuationRing R] [Mul S] (f : R →ₙ* S)
    (hf : Function.Surjective f) : PreValuationRing S :=
  ⟨fun a b => by
    obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := hf a, hf b
    obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b
    exacts [⟨f c, Or.inl <| (map_mul _ _ _).symm⟩, ⟨f c, Or.inr <| (map_mul _ _ _).symm⟩]⟩

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